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.
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!
rzmmm · · focus · HN ↗
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.