3 ms·

This brings to mind a conversation that I've had several times over the years. It goes something like this: > Wouldn't it be cool if we could have code that wo

This brings to mind a conversation that I've had several times over the years. It goes something like this: > Wouldn't it be cool if we could have code that would test itself? > Yeah, if only there were some kind of automated way to encapsulate the requirements of classes and methods that could ensure that they behaved within some known boundaries...? We've had automated unit tests for quite some time, but they are more often called compiler checks. Want your "automated unit tests" to be more comprehensive? Improve your type system and your compiler! With all that said, I do not want to be dismissive of peoples' projects. This is fun and neat.

carlmr 5y ago
The next thing is semi-automatic tests, which you can do with property based testing, fuzz testing, and sanitizers.
sidmitra 5y ago
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...

carlmr 5y ago

The next thing is semi-automatic tests, which you can do with property based testing, fuzz testing, and sanitizers.

sidmitra 5y ago

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