Rust, TLA+, Aesthetics and more

April 5, 2020

Rust, TLA+, Aesthetics and more

It’s been a while I have not put my thoughts in here, so this entry will be a mix of some of the papers or blogs I read recently, some thoughts about Rust and TLA+ because I started trying them both recently, and a few interesting talks I saw recently. The Aesthetics part will be discussed in the blog entry that I read recently and was an interesting reflection on how tools shape our way of thinking.

TLA+

I’ll start by talking about TLA+ because it lead me to other subjects I’ll talk after. I discovered TLA+ after reading a few blog posts seen on HackerNews.

Basically the idea behind TLA+ is that writing software that is correct is extremely hard to do (more so is you include concurrency/parallelism in your software). TLA+ is a high-level language for modeling systems, that relies on math to check the correctness of the model. It has been used successfully by engineers in big company like Amazon and Intel to help them design robust systems.

TLA+ is mainly the work of Leslie Lamport (I did not know about him before), a fairly well-known computer scientist known for his work in distributed systems (and being the initial developer of LaTeX). He received many prizes including the Turing award in 2013.

On The TLA+ Home Page there is lots of resources to start using it, links to the toolbox, an introductory video course and more information to get started. I am currently at the seventh lecture of the introductory course and it is an interesting concept that I’m willing to try to put in practice. I’ll probably come back writing back more on this.

Rust

Rust is the “new” language (since 2010) developed by Mozilla with the goal to have a “safe”, low-level and performant programming language (as an alternative for C/C++). It features quite a few interesting ideas that I find intriguing and I decided to try it out.

What drew me in was:

  • immutability: something that I really like about Clojure as well! In Rust it seems it’s an opt-out feature, if you declare a variable like let x = 0 it is immutable but you can opt-out with the keyword mut (as in let mut x = 0)
  • low-level: I have a very limited exposure to low-level languages (and concepts). I did quite a lot of C in my university classes and an internship in C++ dealing with OpenGL but to be honest I forgot most of it. So that will be a good opportunity to get back to low-level programming.
  • no runtime: I read about that and I have no idea what does this mean in practice but I want to find out! Right now my idea of that is that Rust is embeddable is other programs via C/C++ FFI with no overhead. I hope to be able to call Clojure code from Rust and vice versa (I saw some repos and blog post about it so it seems definitely doable).
  • safe: It seems Rust does a lot of compile time checking to ensure safety and correctness (even for threaded/concurrent program). As far as I understand, it is thanks to is rich type system.

Another good point is that because Rust is a recent language (and good fundings), it has all the niceties like package manager (Cargo), utilities for documentation included (seriously running cargo doc --open is really a nice experience!), nice integrations to the majors editors, installation is very straightforward, so far documentation is really high quality…

I started the Rust book, very nicely done so far (I’m in the middle of chapter 3).

I will be progressing toward the end of this book and then try my hands with it. It should match very well with TLA+ as well.

Blogs

I won’t talk here about all the interesting blog posts I read since the last time I wrote in this blog (a few months ago) but I wanted to highlight and share some very interesting read I had this past few months:

Software, Aesthetics, and Craft: How Java, Lisp, and Agile Shape and Reflect Their Culture

In this post, the author compare the difference between “classical” and “gothic” architecture (real architecture, not software architecture), the elements that characterize both (notably in how much freedom is given to the craftsman) and how we can think about programming language in the same way.

This piece is really nice and I really think you should read it too :)

How I became a better programmer from James Long (creator of Prettier)

This post is like many others on the internet where the author describes how he try to be a better programmer. Very quickly his point his:

  • Find inspiration in other people put keep a critical eye on their work
  • Don’t feel pressured to work all the time, truly revolutionary stuff happens only every few year at best
  • Ignore fluff. Learning syntax and the specific API of a new tool is far less interesting in the long run compared to deep knowledge like algorithm, data structure, how a compiler works, etc
  • Look for previous research about what you are trying to solve, it will probably change your mind in a lot of ways
  • Take on big projects. Get uncomfortable. By trying to accomplish new thing you learn much more

And then he list a few things that helped him be a better programmer:

  • Learn C
  • Write a compiler
  • Learn macros (as in Lisp macro, not C macro)
  • SICP
  • Understand continuations
  • Try a new language

His blog his overall pretty interesting too so go take a look :)

Viability of unpopular programming languages by John D. Cook

The blog posts of John are very interesting (and very short) so if you like a quick read go for it!

In this one he rants about how we rank programming language by popularity (whatever that means) but that does not define how viable that language is (taking Perl, Common Lisp, F# and Erlang as examples).

Misc

Videos

Here are a few conferences talks about Rust

Considering Rust (Jon Gjengset) Making the case for Rust, while also putting emphasis on the weaknesses of it.

Rust at speed - building a fast concurrent database (Jon Gjengset) Discussion about the experience of writing Noria, a high-performance database prototype in Rust

How Rust view tradeoffs(Stephen Klabnik) Great view about the Rust culture and decision making

Books

While reading about TLA+ and Leslie Lamport, I stumbled upon the ACM Digital Library which has free books on programming! Notably one of the latest book is a compilation of the work of Leslie Lamport on concurrency.

Nifty tech tag lists from Wouter Beeftink