Lean is what happens when a programming language and a theorem prover have a baby. Created by Leonardo de Moura at Microsoft Research starting around 2011, Lean lets you write regular code and then prove things about that code, all in the same language. Alok Singh, who wrote a detailed piece arguing Lean is "perfectable" (not perfect, but perfectable), shows how you can define a function that returns 5 and then prove it always returns 5. Most languages can't do this. The compiler itself helps you verify facts about your own code.
The secret sauce is dependent types. Languages without type systems tend to grow them over time. PHP got types in 7.4. Python got type annotations. TypeScript's popularity points to where things are heading. But Singh argues that dependent types are the "proper" foundation for this evolution. In a regular typed language, you might say "this function takes an integer." With dependent types, you can say "this function takes an integer greater than zero, and returns a positive number." The type carries the constraint. Once you have this foundation, you can express any property you want. And on top of that, Lean has built real theorem proving infrastructure. That's what separates it from a language that merely supports dependent types.
Where Lean gets wild is metaprogramming. Singh describes it as almost impossibly smooth. He demonstrates by building custom syntax for tic-tac-toe boards that looks like a visual grid at compile time but turns into proper data structures. You can design layered APIs and hide complexity behind intuitive syntax. The interpretation of that syntax can be swapped easily. Few languages make this kind of thing straightforward.
According to Singh, Lean is the only tool in its class that's actually gaining traction. Coq, Idris, Agda, F*... in his assessment, none of them are really competing anymore. Lean has both raw programming ability and theorem proving. And as Singh notes, with AI making code rewriting easier, a theorem prover becomes the ultimate refactoring tool. If you can prove two pieces of code are equivalent, you can swap them with confidence.
AI coding agents are reshaping how software is built, introducing new challenges around maintaining code quality. The semantic layer for AI coding agents aims to address these issues by improving "narrative hygiene" and enabling more intuitive code interactions.