Hacker News Reader

Comment by fortran77 | Hacker News Reader

Why can't someone write an article about Ada without it having to be about Rust?

Because they overlap almost entiely in use case?

From my own analysis, about a year ago, I do not believe this to be true. Rust is memory safe, but it does not offer the type system that Ada does. The type system is where a large portion of Ada's safety comes from. They're both tackling software/system safety, but from different directions and to different ends.

Additionally, modern Ada (after the introduction of SPARK, what 15 years ago now?) offers even more safety features that I've not seen in Rust, through the form of code contracts. Conttracts which can be used as run-time checks, and (to some degree) as static proofs about the code.

Extend Rust's type system and add a contract mechanism, then it'll have the same use-case that I have for Ada.

SPARK contracts look super interesting. It seems like that could let an optimizer do some great stuff and decrease the mental burden of reasoning about mostly pure functions by calling out specific side effects. What is different about its types? I don't see anything obvious. What I'd miss about rust is the borrowchecker and const by default.

Hmm on further investigation I think most of the use cases I'd have for contracts are met by the borrow checker. Side effects are going to get wrapped in unsafe or be explicit in the function signature.

I would recommend https://www.adacore.com/uploads/books/pdf/ePDF-Implementatio... for more information regarding contracts. There are of course a LOT more, just fire up your preferred search engine and enjoy your findings. :)

> SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.

Contract programming:

- Ada: dynamic

- SPARK: dynamic / static

Run-time errors:

- Ada: dynamic

- SPARK: dynamic / static

Data flow errors:

- Ada: -

- SPARK: static

Strong typing:

- Ada: static

- SPARK: static

Safer language subset:

- Ada: -

- SPARK: static

Strict clear syntax:

- Ada: static

- SPARK: static

---

Additionally, safe pointers in SPARK: https://blog.adacore.com/using-pointers-in-spark and https://arxiv.org/abs/1710.07047.

---

Cryptographic library in SPARK 2014: https://github.com/Componolit/libsparkcrypto.

> libsparkcrypto is a formally verified implementation of several widely used cryptographic algorithms using the SPARK 2014 programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.

---

Ada/SPARK is excellent for real-time and safety-critical software: https://www.rcs.ei.tum.de/fileadmin/tueircs/www/becker/spark... to give you some ideas. It may be a bit outdated in some regards, though, for example: "Next version of SPARK 2014 under development (pointers!).". It is already done! :)

How?

Ada was designed for programming safety-critical, military-grade embedded systems.

Rust was designed as a memory-safe, concurrency-safe programming language, largely to overcome the shortcomings of C++.

Each excels at what it was designed for, but the intended use cases are very different.

Rust is not (currently) being used for aircraft flight control systems--Ada is.

Ada is not (currently) being used for high-performance web browsers and servers--Rust is.

While there are SOME similar design goals in terms of memory safety, concurrency safety, and error prevention, they do not "overlap almost entirely in use case".

Those are good points. While I can see rust flying within the next few years, I dont see it in flight controls for a while yet. That said I'm aware of c++ flight control software which seems insane. And that seems to be the trend. Rust does target embedded so there is no reason not to try and move it in that direction, though ada seems a much better choice.

Agreed. The PicoRV32 mentioned in the article's "WHERE TO GO FROM HERE" section has its own crate: https://docs.rs/picorv32/0.1.3/picorv32/

C/C++ have been great for embedded work, but Ada and Rust are better alternatives in my opinion. They are safer, more powerful, and more secure.

Reply on news.ycombinator.com