Hacker News Reader

Comment by mhh__ | Hacker News Reader

Keep in mind that for this kind of project you want static analysis and formal verification (model checking for example) rather than just day-to-day safety features.

I.e. the Rust this, Rust that spam is a little naive to the task at hand, even though it would be a step up from C

View on HN

NASA even has their own sound static analyzer for memory safety. If you use something like that, and depending on the context, there isn't even necessarily a memory safety advantage to using Rust over C or C++.

https://github.com/NASA-SW-VnV/ikos

It was my understanding that when formal methods were used, they were used on very small subsets of code and not used in general. I do wonder about TLA+ and would love to hear more about how they use such tools.

I know I've seen an older document that specifically prohibited use of malloc that the risk was too great. Is that still the case?

Formal methods are indeed hard. They generally thrive on hardware, software is a wholly different kettle of fish in terms of the size of the problem (the actual methods are often similar, but hardware design generally encourages certain patterns that are easier to analyse)

I'm not related to this project or aerospace, so I can't divine more knowledge than anyone else, although I have seen many coding standards that forbid malloc after some critical time (e.g. no dynamic memory allocation after the plane is off the ground)

Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?

The problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it.

Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.

Because the problem is unsolvable, there is a wide variety of "you can handle it"-ness that a language can have...

Case in point, while it is nice that Microsoft is now playing with Rust, it is quite far away from offering this to Windows developers, https://microsoft.github.io/microsoft-ui-xaml

Advocacy should always be tempered with a bit of hard reality check, otherwise one just ends up scaring possible adopters away.

Yes, but C is one of the languages with the very low amounts of inherent safety. So using a language/tooling that will be offering stricter possibilities of validations of behaviour/more safeguards against unsafe behaviour would likely catch a lot more bugs earlier when they are easier and cheaper to fix.

Reply on news.ycombinator.com