2 ms·
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
by agentultra 7y ago
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.