A New Favorite Language?

I have just finished reading Kevin Hartnett's "The Proof in the Code – How a Truth Machine Is Transforming Math and AI", which is kind of Origin Story of the Lean programming language. On its website, Lean describes itself as "an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code".

I discovered the language more than two years ago and was immediately intrigued, as it had something I missed in other interactions with computers and computer languages. Some rigidity into writing programs. A super theoretic foundation. I've also for decades had a wish to learn more pure mathematics, but I find it hard to grok the mathematical way of thinking. I've been thinking that maybe Lean could help with that, as it's a computer language, and I grok those. The problem is, though, that I've found it tough to get Lean to click with me yet. So, now I have two problems: to understand math and to understand Lean.

A fun thing is that now several interests point to Lean. During the summer, I began to revisit the theory of computation, and I have for a while been working on exploring AI. So, maths (and mathlib>), Theory of Computation (CSLib), and AI come together in Lean. Within AI actually both as a tool for controlling the fallible machines that are LLMs with guarantees for correct code and as the tool AI uses for working within proving open math problems.

My hope is that I, through Lean, will come to explore mathematics like I've always wanted to do.

Reading the last pages of the excellent book, which I recommend to all interested in Lean, I came to think of the computer languages I've come across in my life that have connected with more than just a tool. Do they have something in common? Why those and not something else?

Well, here they are for future thoughts...

Comal-80

The first, and therefore it must start this list

Z80 machine code

I did a lot of programming on the ZX Spectrum, but the thing that amazed my the most, was when I could get a machine code program running. I did not have an assembler, so I wrote assembly code on paper and compiled it into machine code by hand. Crazu stuff.

mic-1 assembly code

During my first year at university, I was introduced to the mic-1 virtual computer from Andrew Tannembaum's book Structured Computer Organization, and learned to program it in assembly language. It was fun!

Mjølner Beta

At university we were also introduced to other educational computer languages created by the instructors (and named after their kids Schwartzbach, Michael .(October 1997). daimiposten - oktober '97), but also to the real object-oriented language and system The Beta programming Language. This introduction also included theoretical introduction to hierarchies and the philosophy of "things in the real world", and modelling of the real world in algorithms and computers. I loved the Beta language but not the very slow and brittle compiler.

Perl

TMTOWTDI and "Easy things should be easy and hard things should be possible". The first time I wrote a Perl script, it worked and seemed linke magick. I keep wondering why I left Perl.

Lisp

The Eternal Flame (God Wrote in Lisp)

Erlang

I have not used it at all, except for a few toy examples, but its very distributed and concurrent nature, its origin, and its robustness towards failures have always intrigued me. And its offspring Elixir. Mystics...

Wolfram Language

Well, it has been my driver for decades for exploring the computational and scientific universe.

Clojure

Lisp main downside has to me always been the lack of easy accessible libraries for regular stuff, Therefore, when Clojure appeared on the scene, I was imediately on it. Also, its creator Rich Hickey is a true guru.

Julia

A modern interest that keeps bubling in the underground of my interests. Where I pushed away from Wolfram Language, Julie would immideaitely pick up the mantel of my daily driver for exploring the computational universe

Lean

Now, we're here at the present day. Lean is the latest entry on this list, and I have a feeling that it will become more and more popular in my tool chest. I just need to "get it" and to that end, there's only one path: hard work.

Notable mentions are Sinclair BASIC, Tcl, FORTRAN, C, Java, R, and lately JavaScript, but they were and are more workhorses for getting stuff done and food on the table.

One more thing: I found this vibe-coded integration of the Wolfram Language and Lean. LeanLink paclet and LinkLink GitHub project. Though I haven't got it to work yet, it could be a fascinating merge of two special systems.