3 ms·
A type checker is a formal proof system. A test determines correctness for a given input. A formal proof system determines correctness for all inputs.
by jdmichal 10y ago
A type checker is a formal proof system. A test determines correctness for a given input. A formal proof system determines correctness for all inputs.
- xapata 10y agoThe are limits to what a formal proof system can do (eg. The halting problem). I also have never met someone who claimed to never need tests because of a powerful type system.
- jdmichal 10y agoI'm not claiming to not write tests. I am claiming that there's a class of tests that do not need to be written if a formal proof system is guaranteeing the results. I don't need to write a test to see that `Math.sin("banana")` behaves properly, because the type system can guarantee that this doesn't happen.