3 ms·
> Types can't (usually) tell us when we accidentally put a "!" in front of a conditional critical point in any 'types vs tests' discussion. strongly typed lang
by awinter-py 7y ago
> Types can't (usually) tell us when we accidentally put a "!" in front of a conditional
critical point in any 'types vs tests' discussion. strongly typed langs can tell you that your program will run w/out crashing but not that they'll be right
(even the 'run w/out crashing' promise turns out to be not always true)
I wonder what tools will evolve in the next 10 years to measure if code is 'semantically correct'. Some sort of function that maps from code to docstrings might be able to check this.
- agentultra 7y agoSemantically correct is important! What kind of semantics? I prefer denotational. Many programmers think in operational semantics. And how does one verify their code? I'm trying to push our review guidelines to ensure developers submit their code/change with an argument as to why it is correct. I got this idea from E.W. Dijkstra who was having a hard time keeping up with his graduate students and colleagues. In order to save his time and sanity he asked them to submit an argument as to why their change was correct. Instead of validating their algorithms, Dijkstra was able to validate their argument and check their proof. One can use unit tests to make this argument. The level of rigor depends on the task on how difficult it would be to convince the reviewer that your change is correct. One can go beyond unit tests and write property tests, make arguments based on the type information, embed proofs in the types, or make more formal arguments by proof if they feel it's necessary. Making unit tests required is a good minimum case I think but is often not sufficient.
- awinter-py 7y agoI've certainly talked myself into 'correcting' unit tests that didn't agree with bad code