Can code "work" but still not be "correct"? For example, I might describe C code that relies on undefined but platform-specifically-reliable behaviours this way
10
1
11
Conversation
Is code that works but has a, so far, unobserved, bug also in this category? Almost all code is subtly incorrect but still works
1
3
Yeah I was going to say, if the threshold is “100% correct” then almost no code works
1
1
(“Enter me!” said Idris and Agda in parentheses)
2
Dependent types can't save you because the specification might be wrong. They might help you reduce the magnitude of your mistakes though (*if* you decide to use them for specification stuff, which is optional).