|
|
|
|
|
|
by maxwells-daemon
2052 days ago
|
|
|
One cool thing about Lean is that the next version is trying to become something like a general-purpose programming language, with the idea of "using proofs to write more efficient code." For example, you might prove that your code never accesses a buffer out of bounds, so you can remove all your bounds checks for efficiency. Another example is implementing recursive functions with induction -- you can implement Fibonacci naively (fib 0 = 0, fib 1 = 1, fib n = (fib n-2) + (fib n-1)) and Lean will rewrite it into an efficient (non-exponential) form. See: https://leanprover.github.io/talks/LeanPLDI.pdf |
|
|