4 ms·
The answer is yes, obviously, due to the Curry-Howard isomorphism. Likewise static type checking obviates unit testing. Granted, most static type systems aren’t
by zarathustreal 3y ago
The answer is yes, obviously, due to the Curry-Howard isomorphism. Likewise static type checking obviates unit testing. Granted, most static type systems aren’t Turing complete so there are some assertions that can’t be made at the type level that can be made at the unit test level, however there are absolutely a handful of languages with type systems that are. Indeed, any language with first-class functions can implement runtime type checking via higher-order predicates and thus obviate the need for unit tests. Is this news?
- Jtsummers 3y agoStatic typing, short of dependent types (and even then you have to use them to their full extent), does not obviate any form of testing unless your programs are trivial. For any non-trivial program, testing is still needed unless you're going to go through formal proofs (which could be embedded into dependent type systems). Otherwise, you can have something which type checks but which still contains logical errors.
- zarathustreal 3y agoYour comment reads like you’re opposing what I said but you’re not actually refuting or addressing any of the points I made..do you have anything to add to the conversation or are you just yelling in the opposite direction?
- efarrer 3y agoHi, I'm the author of the blog post and the paper. I certainly do not argue that static typing obviates unit testing. I agree that both are valuable together. I did however find examples where individual unit tests could be deleted because they didn't test anything that wasn't covered by the static type system. In other words static typing didn't eliminate the need for unit tests (for catching bugs), but it did reduce the number of needed tests (in real world code).
- deleted 3y ago[deleted]
- ReflectedImage 3y agoSo I think you are running on a false premise here efarrer. The false premises is that anyone ships bug free code. It can be done but it's stupidly expensive. Formal methods Z proofs, etc. Unit testing and static typing are 2 different techniques which eliminate bugs. The question that needs to be answered is which of the 2 techniques is the most effective per developer hour spent. Unit tests do not caught all the bugs that static typing would catch nor does static typing catch all the bugs unit tests would catch. That's not an useful observation. Nor is there a moral here that you should be doing both, doing both is expensive and costs $$$.