Hacker News Reader

Comment by ernst_klim | 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.

View on HN

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

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

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

Reply on news.ycombinator.com