Comment by eggy | Hacker News Reader

Comment by eggy | Hacker News Reader

We passed on Rust for Ada/SPARK2014 to write to bare metal on Cortex-M processor for real-time, high-integrity, and verifiable mission-critical software. Rust is making strides to be a future competitor, but it's new to the formal verification tooling and lacks any real world legacy in our domain. Ada's latest spec. is 2022. Other than AdaCore's verified Rust compiler, Rust still does not have a stable language specification like C/C++, Lisp, or Ada, SPARK 2014. I have no doubt that it will start rising to tick all the boxes that Ada/SPARK do right now with their decades of legacy in high-intetrity, mission-critical applications. The mandate to use memory-safe software put into effect this past Jan 1 2026 puts some wind in Rust's sails, but it's more than memory-safety in this domain. Plus, I do not enjoy Rust, but Cargo is nice. We're looking at Lean for further assistance in verifying our work. I think there was and is lot of Rust evangelism that will also carry it forward and boost even more Rust popularity,

Presumably, if you use formal verification then that includes memory safety anyway? Would seem strange if it does not.

Formal verification requires a spec and a very large, very expensive amount of tooling to be developed.

My understand is that both these things are in work, and that neither of these things exist yet.

Yes, and AdaCore's tooling is formally verified and produces reports already familiar to aerospace, railway, and auto auditors for verifying certifications making it attractive to this industry segment of high-integrity apps. Memory safety is taken care of mainly through the features Ada/SPARK2014 offer in creating safe, high-integrity programs, correct.

Yeah right now it’s usually C, but if I had a choice I’d use Ada. I’ve never done a graphical interface with Ada, and I have with OpenGLSC using C.

I’m sure at some point there will be an accepted formal verification toolchain for rust, I hope to never use it.

I've read (from one from one of the people that contribute to Rust afair), that they were involved building formal verification for Rust, and found that the control flow is just so complex that its very hard to use the language like this.

There's this: https://rust-lang.github.io/fls/

But I think the lack of a formal specification is really not as big a deal as it's made out to be. It's one of those "think of a technical reason to justify a decision I've already made" excuses.

Obviously it would be great if Rust does get a full formal specification but I think avoiding it because it doesn't is just silly. C++ has a formal specification... which frequently has bugs and ambiguities. They aren't magically right and either way you're going to need to do a lot of non-formal testing as well as formal verification if you want confidence in a design.

This is true even for domains where formal verification is routine like SystemVerilog. I've seen designs pass formal but fail in simulation or vice versa due to subtle differences in the semantics. (Hopefully that can't happen for Rust but you get the point.)

Rust is not really memory safe if you combine it with external libraries. Too many "unsafe" keywords, and lack of tooling for code analysis and verification.

Edit: With c, you can do memory safety analysis on all system libraries and entire Linux kernel. Some OS kernels, libs and languages do not have dynamic memory allocation at all!

Some languages are memory safe! Learn more about embedded programming!

This is correct. Some widespread libraries leak memory, for example. I love Rust, but I don't think this happens much in Java land.

Rust's definition of memory safety doesn't consider leaks unsafe, which isn't to say your system requirements can't .

Under that rubric, no language is memory safe.

To me Rust is just a nicer language than C. I don't care too much about how easy the language makes memory safety, provided it doesn't make it difficult. But Rust's type system, higher-order functions, polymorphism, macros, etc. make it more pleasant to write than C for complicated programs.

Reply on news.ycombinator.com