> the propositions actually correlate with what people actually want out of the system
My point is that this is the hard part, and writing annotations does nothing to help with this problem.
My point is that this is the hard part, and writing annotations does nothing to help with this problem.
To me, it’s essentially implementing the same code twice in two languages and checking the behavior matches.
If the same person implements both, what are the odds they implement the same bug in both?
Only verification annotations are generally even harder to read and write than the code itself, making it even more difficult to tell if you implemented the proof according to the spec, or just mirrored what the function actually does.