lean4

Yeah, I believe they said they intend for it to be used as a general purpose programming language. I used it to complete Advent of Code last year. There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 ) Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 ) And I'm impressed that you can add to the syntax

Lean4 manages to pull off changing the parser on the fly at compile time. You can add new productions, add new syntax node types, and add new tokens. Then define macros or code to process the additional syntax. Here is a sample I found that adds a simple JSX-like syntax starting around line 93 and then uses it at line 169: https://github.com/leanprover/lean4/blob/master/tests/playgr... I believe most of the language is defined this way, although it is pre-compiled. For more details see the lean4 metaprogramming book: https://github.com/arthurpaulino/lean4-metaprogramming-book

Some quick info for Lean: Homepage: https://leanprover.github.io/ Source: https://github.com/leanprover/lean4 Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)