Hacker News Reader

Comment by pron | Hacker News Reader

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/). 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.

View on HN

> 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.

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.

> 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.)

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.

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.

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.

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.

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

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

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.

True, but if we believe the problem is serious and urgent, then a relatively cheap and quick stopgap is exactly what we need.

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.

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.

Reply on news.ycombinator.com