3 ms·
"They require user help in the form of annotations in cases where they can't prove everything automatically." So, like I said then. Doesn't exist in any practi
by lawnchair_larry 10y ago
"They require user help in the form of annotations in cases where they can't prove everything automatically."
So, like I said then. Doesn't exist in any practical form :) Annotations are clearly a non-starter.
- pron 10y agoRight, because clearly adding some annotations (which is similar in effort to writing test cases) is a non-starter while rewriting hundreds of millions of lines of code in new, immature languages is going to solve the problem faster. And that nonexistent-in-practice approach is commonly used in safety critical software.
- lawnchair_larry 10y agoMark my words. In 10 years, there will be no more adoption of annotations than there is today. If you can't get anybody to use something, it's a non-starter. It doesn't matter why. It just hasn't happened and it wont happen.
- pron 10y agoYou could have said the same about unit tests 20 years ago. The annotations themselves are immaterial; the point is the use of formal methods. Formal methods requires some assistance. Whether you write those as annotations in the code or in a separate file is an implementation detail.