4 ms·

Type checking, compile-time errors won't check if the program you wrote is correct, only that it's internally consistent. That is an entirely different thing th

Type checking, compile-time errors won't check if the program you wrote is correct, only that it's internally consistent. That is an entirely different thing than checking for correctness. You do need a layer of tests that actually try to prove that given some input your program actually does what it's supposed to do. That is hard to automate. Joe Armstrong(of the Erlang fame), talks about this a bit here: https://youtu.be/TTM_b7EJg5E?t=778 https://youtu.be/TTM_b7EJg5E?t=778 I've pointed to a specific timestamp, but there might be more details somewhere else in that talk.

bollu 5y ago
That's untrue. There are type-systems and type-checkers which can check for correctness, as specified by a mathematical formula. This is proof assistants such as Coq[1] work. For example, take a look at fiat-crypto [2], a project that generates code that is correct by mathematical proof, and is now deployed in Chrome. Another famous example is the CompCert [3] compiler, a C compiler along with a correctness proof that the compiler generates assembly which correctly simulates the C semantics. These are based on powerful types as "dependent types" which can encode mathematics and programs in the same programming language, and allow the mathematics to "talk about" the program. The mathematical underpinning is the Curry-Howard-Lambek correspondence. [1] https://coq.inria.fr/ https://coq.inria.fr/ [2] https://github.com/mit-plv/fiat-crypto https://github.com/mit-plv/fiat-crypto [3] https://compcert.org/ https://compcert.org/ [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...