3 ms·

"There are static analyzers that can guarantee -- 100% -- no memory safety issues." This is untrue, at least for any practical interpretation of such a guarant

"There are static analyzers that can guarantee -- 100% -- no memory safety issues." This is untrue, at least for any practical interpretation of such a guarantee. Which product do you think does this? Note that for it to count, it has to return the results before the programmer is dead.

pron 10y ago
https://trust-in-soft.com/products/ https://trust-in-soft.com/products/ (a commercial product from the people who've built Frama-C) Sound static analyzers are not 100% automatic. They require user help in the form of annotations in cases where they can't prove everything automatically. But the work required is similar -- probably less -- than writing tests. Also, note that it's very easy to find all memory safety errors in a sound way -- you just report every pointer and array access that's unsafe. The problem isn't identifying all errors, but proving the memory safety of the cases that aren't (and that's where they may ask for help in the form of annotation -- to convince them of the absence of an error).
- 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 ago
    Right, 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 ago
      Mark 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 ago
        You 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.

pron 10y ago

https://trust-in-soft.com/products/ https://trust-in-soft.com/products/ (a commercial product from the people who've built Frama-C) Sound static analyzers are not 100% automatic. They require user help in the form of annotations in cases where they can't prove everything automatically. But the work required is similar -- probably less -- than writing tests. Also, note that it's very easy to find all memory safety errors in a sound way -- you just report every pointer and array access that's unsafe. The problem isn't identifying all errors, but proving the memory safety of the cases that aren't (and that's where they may ask for help in the form of annotation -- to convince them of the absence of an error).

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 ago
  Right, 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 ago
    Mark 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 ago
      You 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.