4 ms·
One that isn't machine checked to conform to the specification (with Coq or similar). My standard is even higher for programs than it is for mathematical statem
by loup-vaillant 8y ago
One that isn't machine checked to conform to the specification (with Coq or similar). My standard is even higher for programs than it is for mathematical statements, because they tend to be orders of magnitude more complex.
On the other hand, it's okay for a program to not be proven, because it can be useful even if it has bugs.
- AnimalMuppet 8y ago> On the other hand, it's okay for a program to not be proven, because it can be useful even if it has bugs. True, and a very important point. But... if the program has bugs, do they affect the results? Do they affect the results enough to matter? How do you know? In particular, what is your objective proof that the program does what you need it to do? For many programs, such concerns are extreme overkill. For some, though, you have to prove that it does what you need it to.
- loup-vaillant 8y agoThat's where you quit proofs, and start experimenting. I found tests to be extremely effective at rooting out most bugs. Especially if you use property based tests. Programs that do need a proof still have model checkers like TLA+, and proof assistants like Coq.
- AnimalMuppet 8y agoSure, tests are part of what I meant by "objective evidence".