The Best New Programming Language is a Proof Assistant by Harry Goldstein

Fascinating stuff about the Lean’s capabilities as a programming language. In this talk Harry Goldstein explains how the build pipeline in Lean supports powerful metaprogramming - some of which was purposed for the theorem proving capabilities that Lean is commonly known for. As I’m learning Lean for projects in pure math and system modeling, I may also consider it as a general purpose programming language as well.

I wonder how the lifecycle of Lean and similar languages will play out over the next 5-10 years. On the one hand, there is the ever-present risk of the Lisp Curse rearing its head, where the extreme power of the programming languages lead to especially bright but perhaps misguided engineers’ building their bespoke idiolects that are quirky and solve their problems well but don’t contribute to compounding improvements for the community at large, leading to fragmentation and ultimately to less investment in the language’s ecosystem. On the other hand, there are a variety of factors that make me feel a bit of cautious optimism about such a powerful language. First of all, Goldstein’s talk reflects on some of the language features in Lean that make it easier to wrangle with the challenges of metaprogramming. Second, it seems that broadly speaking the ecosystem has changed - people are more aware now of the long-term consequences of quirky over-engineering, and there is a lot of community investment in languages like Clojure because of complementary characteristics like stability. I wonder whether Lean’s position in the world of mathematics will help provide an achor for it to have similar stability. I wonder too what its type system (notably on the other extreme from Clojure’s approach) and its transpiling to C code during its build process (meaning it has great portability) will mean for it and other languages in the long term. Goldstein suggests, with a nod to how maybe this particular language might not be good for beginner programmers, that some of the characteristics of Lean may end up becoming standards for languages to come. A large factor in the future history of this and other languages though, one that looms big, is how generative AI will shape their trajectories. Will there be greater consolidation of language use? Will niche languages that have unique ideas get changes in the sun they might not have otherwise? Time will tell. I’m excited to see what more will come as I learn Lean myself.

Harry Goldstein’s Website