At Nomadic Labs we are proud to create next-gen software … but we are even prouder to help create the next generation of software scientists!
So it’s our great pleasure to host and work with several PhD students, who bring unique perspectives on the technology which they help us to develop, and whose interest in blockchain we are happy to nurture and inform.
In this blogpost, we will ask five questions of one of our students, Colin Gonzalez (and a couple of questions of his supervisor at Nomadic Labs).
Over to you Colin … no the mic is over here … that’s right, you’re on air!
Currently I’m a Ph.D. candidate in Computer Science at the Université de Paris and Nomadic Labs.1 From 2011 to 2014 I did a BSc in Computer Science at the Université Paris Diderot, now Université de Paris. From 2014 to 2015 I took a year to be a Service Civique volunteer, serving in an NGO called Afev which focuses on non-academic education for disadvantaged children. From 2015 to 2017 I did an MSc in Algorithms and Software Engineering with a focus on Programming Languages, at the Université Diderot. During the second year of the MSc, I got a six-month internship with Yann Regis-Gianas at Université Diderot’s Computer Sciences Lab, on the semantics and implementation of a collaborative spreadsheet system. From 2018 to 2019 I worked as a critical software engineer for the Université Diderot Physics Department. There I developed my interests and skills in critical systems, using formal methods to develop embedded software for satellites. In 2019 I joined Nomadic Labs to start my Ph.D.
The topic of my Ph.D. is building tools to develop smart contracts. My main mentor is Yann Regis-Gianas at Nomadic Labs, and I also work with Benjamin Canou from NL and with researchers from the Université de Paris’ Laboratory called IRIF.
One challenge is to make these tools comfortable for end-users unfamiliar with existing smart contract programming languages like Michelson or Ligo. In particular, we see a potential user base in the spreadsheet user community.
The obvious question arises: could we use spreadsheets to design and to build safe and efficient smart contracts? Safety is critical for smart contracts, because they inherently tend to be used in safety-critical applications, and also because by design, their code cannot be modified once they are launched. We intend to use certified compilation and formal methods to make a trustworthy tool.
With respect to efficiency, we intend to use the results of the ESOP‘19 publication, Incremental Lambda-Calculus in Cache Transfer Style by Paolo G. Giarrusso, Yann Regis-Gianas and their coauthors (the incremental lambda-calculus webpage includes the paper and supplementary material). The techniques of the paper could be used to automatically incrementalize smart contracts, improving their efficiency and shortening execution time.
3. What is the value added and innovative side of your PhD thesis (if applicable, in the Tezos blockchain)?
Currently, smart contracts are written in text-based programming languages. People who know programming know how to do this, but what about non-programmers?
Hopefully, a spreadsheet-based tool could make the creation of safe smart contracts more accessible to end users. This could lead a large community of users who are already familiar with spreadsheets being able to launch smart contracts without needing expertise in a `traditional’ programming language.
4. What is the benefit of preparing a PhD and spending most of your time in a private company vs. a University lab?
Both environments are full of brilliant and highly-skilled people. This is key for a young and curious Ph.D. candidate. Many engineers at NL have a Ph.D. diploma, or at least they are very keen on research-oriented topics. This culture of research is ideal to bridge between fundamental sciences and industrial applications.
Transferring scientific breakthroughs to industrial applications is an important challenge. In the context of my Ph.D. at NL, I look forward to developing scientific understanding in consideration of industrial needs. In particular, we expect the results of my Ph.D. to be immediately applicable to implementing Tezos.
I enjoy programming and I enjoy trying out new ideas and seeing them be implemented in a running system! I guess I’m a child of my generation.
Furthermore, direct experimentation is my preferred setup. Often, scientists purposely abstract away technical details. This makes research easier, but then integrating the results back in the real world can be complicated because many technical details remain unclear.
NL embodies the integration of modern computer science along with the best technologies: a philosophy which I find inspiring and want to be a part of.
As a mentor, I try to provide two kinds of input: methodological advice and scientific expertise.
Doing a Ph.D. is learning how to solve complex problems that have not already been solved. This is a new setting for students, who are usually required to work on problems with known solutions. Thus, a Ph.D. student must learn to explore a world of uncertainty, based on a rigorous analysis of the problem in question, and must acquire a deep understanding of the state of the art in the domain.
That’s indeed the second kind of input I provide: with my experience in formal methods and programming languages, I can synthesise the state of our knowledge, typically by having my student Colin read the relevant research papers and interact with the scientific community in the field.
Believe it or not, spreadsheets are the most widely-used programming language!
In VLHCC’05 Christopher Scaffidi and his coauthors published Estimating the number of end users and user programmers, in which they concluded that there would be about 55 million spreadsheets users in the United States of America in 2012, compared to just 13 million professional programmers. Many people with no background in programming can routinely define sophisticated computations using MS/Excel. Many people use spreadsheets to maintain accounts, or even to automate complex accounting processes.
So: what if these spreadsheets could be turned into smart contracts and deployed on the Tezos blockchain?
Not only would this make programming smart contracts easier, but also spreadsheets are a good way to visualize the state of the contract once it is deployed on the chain: such a tool could help democratize blockchains. Perhaps one day we might see people including something like this in their daily workflow!
If spreadsheets are to be used as smart contracts, then we need to make sure their definitions are correct. Unfortunately, spreadsheets can be error-prone, and famous errors in spreadsheets have turned into losses of millions of dollars. Colin’s Ph.D. will provide reasoning tools to help in the simulation and verification of smart contracts, giving mathematically-backed guarantees of correctness before contracts are deployed on the chain (something that should be standard for any smart contract, in fact!).
With his new vision about what structured spreadsheet programming is, Colin might even have an impact on the quality of the spreadsheets written by the spreadsheet industry of the future.
My research affiliation is: Université de Paris, IRIF, INRIA, Équipe-Project π.r2. But as a student, my enrolment is at the Université. ↩