Re:Theorem Proving in Lean [pdf]
by agentultra on Sunday September 29, 2019 @10:59PM
(#21111419)
It's also a useful tool for practising programmers as well!
The documentation for it isn't so great but Lean is a fully dependently typed programming language with a good VM. It is optimized for interactive theorem proving which means the type checker is really fast. I think getting a good native compiler out of it is not far off.
The documentation for it isn't so great but Lean is a fully dependently typed programming language with a good VM. It is optimized for interactive theorem proving which means the type checker is really fast. I think getting a good native compiler out of it is not far off.