Automatically Make Unit Tests

Re:Automatically Make Unit Tests by sidmitra on Wednesday May 19, 2021 @12:03PM (#27210492)

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

I've pointed to a specific timestamp, but there might be more details somewhere else in that talk.

[ Parent | on HN ]

Re:Automatically Make Unit Tests by bollu on Wednesday May 19, 2021 @03:35PM (#27213371)

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/ [2] https://github.com/mit-plv/fiat-crypto [3] https://compcert.org/ [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[ Parent | on HN ]