Hacker News Reader

>Rust covers the worst of errors without much cognitive overhead, and zero runtime overhead.

Ahm, Rust is much worse than SPARK in case of covering errors, and its runtime overhead is no less than that of Ada.

>Not having a fallback system in the event of systemic failure? Unheard of in real satellite systems.

The bad thing about software errors is that fallback systems doesn't help with them. If your computer says not to turn on the thrusters until 100 meters below ground, you will crash. If you have a software-controlled stuff and software behaves badly — you are doomed, and Ada has a huge advantage here, that's why it's still used in aerospace.

>Ahm, Rust is much worse than SPARK in case of covering errors, and its runtime overhead is no less than that of Ada.

Can you elaborate? It's not often that they see valid critiques of Rust on HN, and it would be interesting (to me at least) to add to the data bank.

SPARK lets you write proofs - you can write different implementations of a function and prove at compile time they match some specification. An example of this is here: https://blog.adacore.com/gnatprove-tips-and-tricks-proving-t...

Here's another post with some examples: https://blog.adacore.com/taking-on-a-challenge-in-spark

There's a good book, Building High Integrity Applications in SPARK, that goes through things in detail. It's a good read for any programming language user to mine for ideas or explore how similar problems could be solved in their language: https://www.cambridge.org/core/books/building-high-integrity...

>Can you elaborate? It's not often that they see valid critiques of Rust on HN, and it would be interesting (to me at least) to add to the data bank.

Ehm, SPARK has a full proof capabilities, pretty much like you have in Coq (and SPARK integrates with Coq). With SPARK you can prove your code is correct, with Rust you can't, and there is nothing like Frama-C/SPARK available for rust.

In Ada12/SPARK14 you have statically checked Hoare triplets (in Ada contracts are ensured in runtime sometimes tho), you can ensure that your output array is sorted in the type system and prove it statically, you can ensure all sorts of invariants statically.

I like rust, but it's nowhere near proving correctness since it has neither dependent types (like F star/Low star` has), nor dedicated proof system (like Frama-C/SPARK). You can compare Rust to Ada, though Ada is pretty awesome two and have many features Rust lacks (contracts, subtypes, parametric modules).

And, even if you don't go 'full platinum level proof' (proof of all the High-Level specs of your software) in SPARK you can still enjoy, without too much effort: - proof of no read access to uninitialized variables - proof of absence of runtime errors (overflow, underflow, array out of bound, incorrect conversion...) - proof of type predicates/invariants, asserts, pre/post conditions... - Less known, you can specify and verify 'data provenance' with 'this function's result depends on parameters a and b c' aspects, and you can also specify and verify global variables access (global_in, global_out).

This with a language that supports tasking, generics, and oop natively...

And proof on access types (pointers) are on the way.

Really amazing tech to work with.

This is a misleading comment, because it oversells Rust and criticises Ada unfairly. Ada and SPARK have a track record of being used to build safety critical systems, unlike Rust.

Rust might seem like a big win compared to the average C or even C++ projects due to its memory-safety guarantees, but at the end of the day the only thing it has on Java or Python is protection from data races. It also has some type system features which enable writing robust code, but SPARK is in a different league.

"I would never, ever, use Ada for a non-academic project including those for embedded systems headed to space."

"Failure should be expected and using a very strict language will help, but is ultimately only a crutch. It comes with a lot of cognitive trade offs."

The best study I ever saw doing comparisons put Ada at safer and cheaper to use for critical software:

http://archive.adaic.com/intro/ada-vs-c/cada_art.pdf

SPARK proves absence of certain kinds of problems that even experts run into. You can do that with static analyzers and such on subsets of C. They tend to cost way more than a SPARK Pro license. SPARK the language is also easier to learn than mastering C with all its dark corners. If not proof, they can also do contract-based, test generation and/or fuzzing with contracts as runtime checks. Will knock out tons of errors.

So, I think the evidence is against your claim so far. And, as to this:

"What happens in the real world? C."

COBOL, Excel, Visual Basic 6, C, C++, Java, and .NET all have piles of code out there. That mean any one being dominant proves its the best? Nah, that happens for social and economic reasons, esp when ecosystem is established. Especially for C. It's worth considering alternatives such as Ada/SPARK, Rust, and D.

I'm also for making the alternatives plug into and use C ecosystem nicely. Maybe even compile to it to leverage its tooling. When that happens, the alternative will strictly be better than C for being able to use all of its ecosystem strength with as little or much weaknesses as integrators want to bear.

Ada is a positevly amazing language. The only real complaint that can be made about it is the dearth of libraries/non-existent package management and the weird FSF vs. AdaCore compiler licensing issues.