> You can ask, why is it so painful to give a formal proof of correctness of your program? It's not! It turns out that the dependently-typed lambda calculus i

> You can ask, why is it so painful to give a formal proof of correctness of your program? It's not! It turns out that the dependently-typed lambda calculus is sufficient. See the research into Lean[0]. It seems we had discovered a portal called, Curry-Howard. You can throw in theorems in one side and out come proofs on the other. Programs are mathematical objects. And programming is a subset of mathematics. I like to think of it as an applied mathematics. It just so happens that practitioners of this language don't require knowledge of the other side of the portal in order to write their proofs. They just write their proofs without any theorems, or at best, a large suite of examples. To me writing proofs is programming. [0] http://leanprover.github.io/ http://leanprover.github.io/