5 ms·

Because they overlap almost entiely in use case?

Jtsummers 7y ago
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.
- galangalalgol 7y ago
  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.
- galangalalgol 7y ago
  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.
- johnisgood 7y ago
  I would recommend https://www.adacore.com/uploads/books/pdf/ePDF-ImplementationGuidanceSPARK.pdf 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 https://blog.adacore.com/using-pointers-in-spark and https://arxiv.org/abs/1710.07047 https://arxiv.org/abs/1710.07047. --- Cryptographic library in SPARK 2014: https://github.com/Componolit/libsparkcrypto 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/spark2014-intro.pdf 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! :)
thesuperbigfrog 7y ago
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".
- galangalalgol 7y ago
  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.
  - thesuperbigfrog 7y ago
    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/ 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.

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.

galangalalgol 7y ago
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.
galangalalgol 7y ago
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.
johnisgood 7y ago
I would recommend https://www.adacore.com/uploads/books/pdf/ePDF-ImplementationGuidanceSPARK.pdf 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 https://blog.adacore.com/using-pointers-in-spark and https://arxiv.org/abs/1710.07047 https://arxiv.org/abs/1710.07047. --- Cryptographic library in SPARK 2014: https://github.com/Componolit/libsparkcrypto 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/spark2014-intro.pdf 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! :)

thesuperbigfrog 7y ago

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

galangalalgol 7y ago
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.
- thesuperbigfrog 7y ago
  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/ 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.