The Rust Review: Dr. Ittay Weiss on Embracing Rust and Leaving Academia

Welcome to our Rust Review series, where we embark on a journey through the intricate world of Rust programming with some of the brightest minds in the field. In this exclusive series, we'll be hosting guest bloggers who are making waves in the Rust community, getting their unique insights, experiences, and stories behind their code.

First in line is the esteemed Dr. Ittay Weiss, a seasoned Rust Developer currently shaping the future of code at Stockly in the city of Paris, France. With a wealth of expertise and a passion for pushing the boundaries of what Rust can achieve, Dr. Weiss offers a unique perspective that sets the tone for the excellence we aim to bring to you in each instalment of our Rust Review series. 

Quitting Academia for a Career in Software Engineering

Two years ago I decided to quit my university lecturer position and revamp my career as a software engineer. Ok, yes, I’ve made that decision before. Numerous times. But two years ago, I actually followed through. Ok, yes, there have been some other circumstances that nailed the coffin with my old career RIPing in it. Reasons and circumstances aside, I was at the doorstep of an entirely new world I knew very little of. There are many lucrative paths to follow once inside, and equally many friends and acquaintances, armed with good intentions, seem to profess that the best way forward is to choose the niche they just so happen to be occupying.

I was getting dizzy. I was also getting worried. When I chose my first career, I was young and stupid. Now I am older and, hopefully, less stupid. Enough to want to make informed choices. The title is enough of a spoiler alert; I am today a Rust developer at Stockly, a startup company in Paris, and this is among the best things that ever happened to me. So, why software development? Sure, for a mathematician it isn't exactly that far off. All that logical thinking, attention to detail, enjoying banging my head against a hard problem until something breaks, and love of pedantry are skills that lend themselves useful when getting a computer to do what you want it to do. After all, I am certainly not the first mathematician to switch teams. I had some coding skills in C/C++ and Python that I had picked up through the years and I knew that I enjoyed programming. But I needed to make a good choice for the language. I was fortunate enough to be able to relocate myself to an environment where I could safely experiment for several months with different aspects of software development. I vigorously exposed myself to the more (and less) trendy developments in the field as I was learning the ropes.

Choosing Rust - A Mathematician's Perspective

One day I came across Rust. Ok, sure, it has a cool name. But what is that 'ownership' business? That sounded new. Oh, it promises superb performance without the pain and dangers of managing the memory myself. It started to sound like wishful thinking. I was sceptical. But not for long. It didn't take me long to get to chapter 4. The sensation of witnessing a marvellous revelation progressed with each passing sentence. Three rules. So simple. So right. That sensation rested comfortably on my, admittedly limited, yet poignant, experience with C. It is so tempting to convince yourself that you are a disciplined enough programmer to guard your precious C code from the perils of memory leaks, races, and deadlocks, but woe to those who dare act upon such hubris. Rust's ownership does, clearly, offer a refreshing new approach and many (smart) people say it works. That would have already been enough to get me to continue to focus my attention on this new phenomenon, but there was more. My maths senses were tingling.

My research area as a mathematician is category theory. Logic and foundations, and the relationship between computer science and mathematics, always interested me. Variables in most computer languages act similarly to the way mathematical variables act in proofs. Particularly the non-mutable variants, but that is really just some functional programming mojo. Nothing new. In any case, a programming language has, at least heuristically, an underlying logic. Superficially, it is just boolean logic. Less superficially, it is some variant of intuitionistic logic. I like to think of the differences between programming languages in terms of the differences between their underlying logical systems. Rust smelled funny. It wasn't good old boolean logic.

Problem-Solving in Rust and Mathematics

It didn't take me long to formalise the logical principles and I immediately recognised it as very closely related to linear logic. That was very exciting. In a nutshell, linear logic treats variables as finite resources, where it matters how many times you use a variable. In particular, you can run out of the stuff held in the variable while still in the middle of a proof. This is very similar to Rust's concept of moving values, which is a common stumbling block for newcomers to the language. As I was programming in Rust, I was thinking in linear logic, rather than boolean logic. I liked that a lot. Ever since I abandoned the axiom of choice as a valid principle of proof, about four years ago, I found boolean logic to be less and less relevant in the real world. It was delightful to see how a fresh approach to solving classical memory management problems led to the development of a language that dispenses with classical logic. That was beautiful.

The memory management system is Rust's USP, and I was very happy with its theory and the way it works in practice. Surely, I needed some time to get used to some unexpected "value was moved here" errors by the friendly compiler. And what a refreshingly friendly compiler it is. All the time trying to help you. Teaching you with each step. It took some time, but we are now good buddies. It was easy to see why developers rank the Rust environment so highly. So, Rust captivated me with a unique approach to memory management that is closely tied to awesome mathematical principles, and a superb working environment. But there is more than that to a programming language. In particular, its programming paradigm and typing system. Clearly, I was expecting thought and design behind these as well, and I was not disappointed.

The Rust Development Environment

Rust is strongly and statically typed. Luckily (I believe), my first language for learning programming was C, and not Python. Rust's typing system felt extremely natural and very mature. Designed to encourage the construction of new types on the fly, and incorporating paradigms of computation via type modification, programming in Rust involves a great deal of thought and design of the ambient type infrastructure prior to solving the problem at hand. That resonated strongly, again, with category theory. It reminded me of the quote from the French mathematician Alexander Grothendieck regarding his view of solving problems in mathematics, comparing the process to that of cracking open a nut: 

"The first analogy that came to my mind is of immersing the nut in some softening liquid, and why not simply water? From time to time you rub so the liquid penetrates better, and otherwise you let time pass. The shell becomes more flexible through weeks and months – when the time is ripe, hand pressure is enough, the shell opens like a perfectly ripened avocado!"

Mathematically, working with a strongly statically typed language felt like the usual way of thinking category theoretically. Solving a problem in mathematics often involves applying functors to it, passing it around from one category to another. The idiomatically frequent use of ‘impl From<T> for S’ is quite similar. In Rust, a well organised type infrastructure, with correctly implemented ‘From’s, enables one to think globally in order to efficiently and harmoniously solve local problems. Further Rust idioms recognise the difference between intentional and extensional types. For instance, Option<T> is isomorphic to Result<R, ()>, superficially pointing at code duplication, but, the intention is vital, and so no attempt is made to reduce Option<T> to Result<T, ()>. Category theory, too, recognises the importance of making a clear distinction between isomorphic things, so once again I felt in very familiar territory.

Finding Harmony in Rust Development

To conclude, by switching from mathematics research to software development in Rust, I found myself smoothly transferring my skills and thought patterns nearly verbatim. Working with Rust is like operating mathematically in an ambient linear logic, using a well-structured type system that enables me to think and act functorially in order to solve problems, and produce highly performant code. And all of this within a working environment more pleasant than I dared to imagine could exist.

Links:

https://arxiv.org/abs/2303.05491

https://medium.com/@martriay/rust-and-linear-types-a-short-guide-4845e9f1bb8f

https://webusers.imj-prg.fr/~leila.schneps/grothendieckcircle/Mathbiographies/mclarty1.pdf