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 a

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...