2 ms·
It is a question of completeness; the proof your provide must be complete for your case while your unit tests do not have to be. What you want is that your code
by tluyben2 9y ago
It is a question of completeness; the proof your provide must be complete for your case while your unit tests do not have to be. What you want is that your code does what you intend to do and in languages like Coq, Idris and f* you have to provide a proof for it that covers not some subset fuzzing test (or physics) proof but a full covering (or math) proof. Simplified and this is a subject of a lot of CS research as we know it is needed.
Before I insult anyone who studied physics; the above idea that physics just tries something 1000 times and then considers it true while math makes it all covering is a thing Dijkstra used to say when teaching at TUE in Eindhoven NL and I always remembered it as it is empirical vs math.
I use the much lighter TLA+ myself as indeed only(?) French rail pays for actual formal verification in software.
- mjburgess 9y agoA total aside here, but this Humean view of science isn't really accurate, though often repeated. It isnt that something happens 1000x. It's that we arrive at a causal explanation of how something happens and then this explanation is confirmed across 1000 instances, so on the basis of this causal explanation being accurate enough, it is reasonable to predict the 1001. The difference is that in the Humean "1000x therefore 1001" case there is no reason to suppose 1001. If the world were really just these sequences it would be inexplicable. Rather, the world has a causal structure and it this that we better understand by making inferences. cf. induction vs. abduction