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.
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.
> 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.
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.
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.
Unless the function is a public API and unused in the library (i.e. if the function is used by code that expects it to do Y), it won't pass verification.
If it is public API, it indeed can pass. This is similar to theorem provers - if you get your axioms or theorems wrong, you can incorrectly "prove" things. But verifiers are still useful because most of the code has larger internal surface than external surface.
MeetingsBrowser · · focus · HN ↗
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 · · focus · HN ↗
MeetingsBrowser · · focus · HN ↗
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.
afdbcreid · · focus · HN ↗
MeetingsBrowser · · focus · HN ↗
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.
afdbcreid · · focus · HN ↗
If it is public API, it indeed can pass. This is similar to theorem provers - if you get your axioms or theorems wrong, you can incorrectly "prove" things. But verifiers are still useful because most of the code has larger internal surface than external surface.