2 ms·
What about the performance characteristics of the Lean programs? I know it is a natively compiled language, but is the code it produces comparable to that of mo
by ibobev 6mo ago
What about the performance characteristics of the Lean programs? I know it is a natively compiled language, but is the code it produces comparable to that of modern system programming languages in terms of performance?
- ted_dunning 6mo agoOddly enough, most uses of Lean never actually run the program. The fact that it type checks is enough to prove the theorem in question. That said, if execution is seriously required for your problem along with strong logic on the side, you may prefer Dafny which transpiles the computation part of your proof to C++ or Go.
- ibobev 6mo agoBut still, Lean is executable and can be used as an ordinary programming language.