3 ms·
the vast majority of such annotations are checked though. There's generally three kinds of annotations in formal proof systems: assertions about inputs that can
by rcxdude 24d ago
the vast majority of such annotations are checked though. There's generally three kinds of annotations in formal proof systems: assertions about inputs that cannot be checked by the system, statements of propositions that want to be checked, and proofs that those propositions follow from the assertions. The proofs are checked by the system, so writing them is mainly just tedious and difficult, not really a source of error. What needs to be verified carefully is that the assertions are true, and that the propositions actually correlate with what people actually want out of the system. The mark of how effective a formal verification system is is in how strong of a proposition can be proven from how small a set of assertions. (well, and then how difficult it is to write the proofs).
- MeetingsBrowser 24d ago> 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.
- rcxdude 23d agoTo me it seems easier than proving the code does something useful without pinning down what that actually is.
- MeetingsBrowser 23d agoI agree on paper, but in practice most verification annotations in real code require a PhD to understand. 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.