4 ms·
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be
by jkhdigital 2mo ago
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.
- deterministic 2mo agoLEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct. In other words, proving something is essentially the same thing as type checking. It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)