3 ms·

It's worth mentioning that there are sound static analysis tools that guarantee no undefined behavior in C programs (e.g. https://trust-in-soft.com/ https://tru

by pron 7y ago

It's worth mentioning that there are sound static analysis tools that guarantee no undefined behavior in C programs (e.g. https://trust-in-soft.com/ https://trust-in-soft.com/). Much cheaper and more realistic than a rewrite. Tenable or not, much of the software we rely on will remain written in C in the next few decades.

deleted 7y ago
[deleted]
0815test 7y ago
> Much cheaper and more realistic than a rewrite. I really have to dispute this, these tools are not simple to use. You'll probably have a far easier time rewriting the code piecemeal, i.e. function-by-function (which will involve a lot of unsafety initially, since you're not using the idiomatic global patterns of a memory-safe language!) and then refactoring into something idiomatic for the language you're using. Projects like Firefox are basically taking a similar approach, only "rewriting" small portions of the codebase that can be deployed immediately once rewritten. Where similar tools might be useful is for preventing logic-related issues that are not encompassed under simple memory safety. Unfortunately it's still not possible to endow, e.g. Rust code with automatically-checkable proofs, showing that the logic in the code preserves some appropriate conditions/invariants; while this is feasible, e.g. in Agda or Idris. Hopefully by the time these concerns become pressing, practical memory-safe languages will also offer this.
- pron 7y ago
  When you want to verify functional properties these tools are not easy to use. For safety, they are easier than a rewrite and largely automatic. Large, sensitive codebases have been verified (for undefined behavior, not functional correctness) relatively quickly. In general, they cover more ground significantly more quickly and cheaply than a rewrite.
titzer 7y ago
> are sound static analysis tools that guarantee no undefined behavior in C programs Proof left as an exercise for the reader, maybe? Seriously, UB is a very, very pernicious problem and without a formal specification of C/C++ and a machine-checked proof that this analysis is sound and complete, I am not going to believe it. The academic research community still regards this as an unsolved problem. (It's a shame, too. With UB, we did this to ourselves.)
- pron 7y ago
  You could also say that you don't trust the compilers of safe languages, or their unsafe bits, to be correct. The guarantee here is about as strong. But the situation is not binary, and what we want is the cheapest way to at drastically reduce UB, even if you don't believe the guarantee rises to the level of being absolute.
  - titzer 7y ago
    The burden of proof is quite literally on those making claims, not on me to "not trust" them. There are certified compilers with machine-checked proofs of correctness (e.g. CompCert). That is a whole other level assurance than prose proofs and hand-wavy informal reasoning. It is probably true that most "safe" languages have some holes in them; e.g. Java does.
    - pron 7y ago
      Fine, but the same burden exists for both sound static analysis tools and safe languages. There's no reason to doubt the claims of one yet accept the claims of the other.
      - titzer 7y ago
        As automated theorem proving and machine-checked proofs are making rapid progress, the burden is increasing. In the beginning, not much was required in the way of proof about a language's type system. Then came systematization and de facto standardization of programming language semantics, along with a standard way of proving things about type systems (typically, small-step semantics, progress and preservation lemmas). Soon, at least in academic papers, it became the norm and almost required to provide formal proofs of type safety. Those languages and systems that lacked proofs often had holes in them. Nowadays, like I alluded to in my original comment, the burden of proof (quite literally) is being ratcheted up even higher, with machine-checked proofs becoming mainstream in academic circles. So in that context, your original comment that these systems are "guaranteed" to be sound is not yet at the level of proof that I would accept. I have reasonable doubts, because dealing with UB in C/C++ is still an open problem.
clouddrover 7y ago
That said, I think there's a large amount of software that's possible to rewrite in reasonable time frames if the authors commit to it. And software with many individual components can be gradually rewritten. Firefox is starting to use components written in Rust like Stylo and WebRender. Mozilla has an Oxidation project for bringing more Rust-based components to Firefox: https://wiki.mozilla.org/Oxidation https://wiki.mozilla.org/Oxidation
- pron 7y ago
  Sure, but sound static analysis can also be adopted gradually, and being quicker and cheaper, requires a smaller commitment from the authors.
Cthulhu_ 7y ago
For sure it will increase the quality and predictability of C codebases, and I would definitely recommend static analysis tools in any language. But it's a stopgap measure, it does not solve the root cause. It has to be made impossible to make mistakes, which is what newer languages are trying to enforce.
- pron 7y ago
  True, but if we believe the problem is serious and urgent, then a relatively cheap and quick stopgap is exactly what we need.
  - pjmlp 7y ago
    Except the first hurdle is to win the religous war against such tools, lint exists since 1979 after all. According to Herb Sutter's question to the audience a couple of years ago at CppCon, JetBrains and ISO C++ surveys, developers and corporations that actually care about static analysis tooling are the exception and not the norm.
    - pron 7y ago
      I totally agree, but safe languages have to climb a hill at least as high as well, and it might even be the same hill. I just think it's worth mentioning that if this kind of safety is important to you, then there are alternatives that are cheaper than a rewrite. Getting people to 1. care about the problem and 2. accept that there are tools that can help them -- be they safe languages or sound static analysis -- is, indeed, a hurdle.

by pron 7y ago

deleted 7y ago

[deleted]

0815test 7y ago

> Much cheaper and more realistic than a rewrite. I really have to dispute this, these tools are not simple to use. You'll probably have a far easier time rewriting the code piecemeal, i.e. function-by-function (which will involve a lot of unsafety initially, since you're not using the idiomatic global patterns of a memory-safe language!) and then refactoring into something idiomatic for the language you're using. Projects like Firefox are basically taking a similar approach, only "rewriting" small portions of the codebase that can be deployed immediately once rewritten. Where similar tools might be useful is for preventing logic-related issues that are not encompassed under simple memory safety. Unfortunately it's still not possible to endow, e.g. Rust code with automatically-checkable proofs, showing that the logic in the code preserves some appropriate conditions/invariants; while this is feasible, e.g. in Agda or Idris. Hopefully by the time these concerns become pressing, practical memory-safe languages will also offer this.

pron 7y ago
When you want to verify functional properties these tools are not easy to use. For safety, they are easier than a rewrite and largely automatic. Large, sensitive codebases have been verified (for undefined behavior, not functional correctness) relatively quickly. In general, they cover more ground significantly more quickly and cheaply than a rewrite.

titzer 7y ago

> are sound static analysis tools that guarantee no undefined behavior in C programs Proof left as an exercise for the reader, maybe? Seriously, UB is a very, very pernicious problem and without a formal specification of C/C++ and a machine-checked proof that this analysis is sound and complete, I am not going to believe it. The academic research community still regards this as an unsolved problem. (It's a shame, too. With UB, we did this to ourselves.)

pron 7y ago
You could also say that you don't trust the compilers of safe languages, or their unsafe bits, to be correct. The guarantee here is about as strong. But the situation is not binary, and what we want is the cheapest way to at drastically reduce UB, even if you don't believe the guarantee rises to the level of being absolute.
- titzer 7y ago
  The burden of proof is quite literally on those making claims, not on me to "not trust" them. There are certified compilers with machine-checked proofs of correctness (e.g. CompCert). That is a whole other level assurance than prose proofs and hand-wavy informal reasoning. It is probably true that most "safe" languages have some holes in them; e.g. Java does.
  - pron 7y ago
    Fine, but the same burden exists for both sound static analysis tools and safe languages. There's no reason to doubt the claims of one yet accept the claims of the other.
    - titzer 7y ago
      As automated theorem proving and machine-checked proofs are making rapid progress, the burden is increasing. In the beginning, not much was required in the way of proof about a language's type system. Then came systematization and de facto standardization of programming language semantics, along with a standard way of proving things about type systems (typically, small-step semantics, progress and preservation lemmas). Soon, at least in academic papers, it became the norm and almost required to provide formal proofs of type safety. Those languages and systems that lacked proofs often had holes in them. Nowadays, like I alluded to in my original comment, the burden of proof (quite literally) is being ratcheted up even higher, with machine-checked proofs becoming mainstream in academic circles. So in that context, your original comment that these systems are "guaranteed" to be sound is not yet at the level of proof that I would accept. I have reasonable doubts, because dealing with UB in C/C++ is still an open problem.

clouddrover 7y ago

That said, I think there's a large amount of software that's possible to rewrite in reasonable time frames if the authors commit to it. And software with many individual components can be gradually rewritten. Firefox is starting to use components written in Rust like Stylo and WebRender. Mozilla has an Oxidation project for bringing more Rust-based components to Firefox: https://wiki.mozilla.org/Oxidation https://wiki.mozilla.org/Oxidation

pron 7y ago
Sure, but sound static analysis can also be adopted gradually, and being quicker and cheaper, requires a smaller commitment from the authors.

Cthulhu_ 7y ago

For sure it will increase the quality and predictability of C codebases, and I would definitely recommend static analysis tools in any language. But it's a stopgap measure, it does not solve the root cause. It has to be made impossible to make mistakes, which is what newer languages are trying to enforce.

pron 7y ago
True, but if we believe the problem is serious and urgent, then a relatively cheap and quick stopgap is exactly what we need.
- pjmlp 7y ago
  Except the first hurdle is to win the religous war against such tools, lint exists since 1979 after all. According to Herb Sutter's question to the audience a couple of years ago at CppCon, JetBrains and ISO C++ surveys, developers and corporations that actually care about static analysis tooling are the exception and not the norm.
  - pron 7y ago
    I totally agree, but safe languages have to climb a hill at least as high as well, and it might even be the same hill. I just think it's worth mentioning that if this kind of safety is important to you, then there are alternatives that are cheaper than a rewrite. Getting people to 1. care about the problem and 2. accept that there are tools that can help them -- be they safe languages or sound static analysis -- is, indeed, a hurdle.