At the start of this summer, I began learning Lean4, a theorem proving and programming language.
Needless to say, it’s probably the best language that I’ve had the joy of programming in.
The main use for Lean4 is to prove theorems using ideas from dependent type theory (DTT).
Specifically, it is an application of the Curry-Howard isomorphism/observation which states that programs are proofs, and one can formally prove a theorem by finding inhabiting terms (which represent proofs) for “types” (which represent propositions).
However, basic non-dependent type theory by itself is not very expressive, and becomes infinitely more expressive under the DTT framework, which allows types to “depend” on values.
Lean4 also supports the following paradigms: functional programming and metaprogramming, and the core philosophy of the language probably revolves around extensibility. To support the expressiveness of mathematical syntax, there is a very powerful syntax manipulation / creation API.
Together, these ideas form probably one of the coolest and satisfying languages to program in. Namely, you can prove theorems, create code which manipulates code (metaprogramming), parse your own DSL, etc, all within a functional programming paradigm! More recently, it has gained quite a bit of traction for being the language of choice in AI / formal methods applications.