4 ms·

I have long been critical of verification tools requiring annotations. Humans cannot write correct code, so asking them to write correct proof annotations seems

I have long been critical of verification tools requiring annotations. Humans cannot write correct code, so asking them to write correct proof annotations seems futile. But maybe this changes in the age of LLMs. A deterministic check to let LLMs verify the correctness of an API could improve the success rate of large scale refactors or performance optimizations. Exciting!

afdbcreid 17d ago
You seem to have misunderstood the idea. The entire idea of proof annotations is that they are not manual. Rather, the verifier checks you fulfill the preconditions for the method you calls, and it checks inside the method that if the preconditions are fulfilled then the postconditions are too. This just helps the verifier reason locally. At the end besides more burden, the only thing you really need to check is the top-level annotations, like any formal verifier.
- MeetingsBrowser 17d ago
  > the only thing you really need to check is the top-level annotations Sorry if I wasn’t clear. My point is that the annotations are manual and inherently prone to error. If humans could correctly write annotations according to a spec, we wouldn’t need verifiers at all. We could just write correct code directly. There is an argument to be made that the annotations are a smaller surface than full blown code and therefore easier for humans to reason about. However, in practice formal verification tools and annotations are far more obscure than regular code. Thousands of people write and review code both professionally and as a hobby. But most people writing verifier annotations have a PhD in some field adjacent to formal verification.
  - rcxdude 17d 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 17d 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 16d ago
        To me it seems easier than proving the code does something useful without pinning down what that actually is.
        MeetingsBrowser 16d ago
        I 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.
  - afdbcreid 17d ago
    You were clear, and you were wrong. The annotations are checked like I said, you cannot break the guarantees using them. If they're incorrect they won't pass verification. They just help the verifier.
    - MeetingsBrowser 17d ago
      Sorry I’ll try to put it simply. Programmer intends to write code that does Y, but writes code that does X. Then they make the same mistake again and write an annotation that verifies the function does X. Verification passes, but the code does the wrong thing.
rzmmm 17d ago
I think it provides best bang for buck when the annotation is "obviously correct" but the implementation is complex. For example if you are trying to prove that your new sorting algorithm yields sorted list for all inputs. If there is as much annotations as there is code, then testing is better tool for the job than verification.

afdbcreid 17d ago

You seem to have misunderstood the idea. The entire idea of proof annotations is that they are not manual. Rather, the verifier checks you fulfill the preconditions for the method you calls, and it checks inside the method that if the preconditions are fulfilled then the postconditions are too. This just helps the verifier reason locally. At the end besides more burden, the only thing you really need to check is the top-level annotations, like any formal verifier.

MeetingsBrowser 17d ago
> the only thing you really need to check is the top-level annotations Sorry if I wasn’t clear. My point is that the annotations are manual and inherently prone to error. If humans could correctly write annotations according to a spec, we wouldn’t need verifiers at all. We could just write correct code directly. There is an argument to be made that the annotations are a smaller surface than full blown code and therefore easier for humans to reason about. However, in practice formal verification tools and annotations are far more obscure than regular code. Thousands of people write and review code both professionally and as a hobby. But most people writing verifier annotations have a PhD in some field adjacent to formal verification.
- rcxdude 17d 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 17d 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 16d ago
      To me it seems easier than proving the code does something useful without pinning down what that actually is.
      - MeetingsBrowser 16d ago
        I 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.
- afdbcreid 17d ago
  You were clear, and you were wrong. The annotations are checked like I said, you cannot break the guarantees using them. If they're incorrect they won't pass verification. They just help the verifier.
  - MeetingsBrowser 17d ago
    Sorry I’ll try to put it simply. Programmer intends to write code that does Y, but writes code that does X. Then they make the same mistake again and write an annotation that verifies the function does X. Verification passes, but the code does the wrong thing.

rzmmm 17d ago

I think it provides best bang for buck when the annotation is "obviously correct" but the implementation is complex. For example if you are trying to prove that your new sorting algorithm yields sorted list for all inputs. If there is as much annotations as there is code, then testing is better tool for the job than verification.