Ask HN: When Ada/SPARK, then why Rust?
9 comments
> what was the reason for inventing Rust?
There will always be new programming languages. In case of Rust the innovation was compile-time dynamic memory management, which then was not available in Ada; but Ada is catching up, see e.g. https://blog.adacore.com/using-pointers-in-spark.
> Why does our industry get so enthused with shiny new things
Innovations can give better opportunities to those who use them smartly. Often, the hype around a technology is so great that the industry is forced to show at least a minimal commitment to appease staff and investors and to not appear old-fashioned (whether justified or not).
There will always be new programming languages. In case of Rust the innovation was compile-time dynamic memory management, which then was not available in Ada; but Ada is catching up, see e.g. https://blog.adacore.com/using-pointers-in-spark.
> Why does our industry get so enthused with shiny new things
Innovations can give better opportunities to those who use them smartly. Often, the hype around a technology is so great that the industry is forced to show at least a minimal commitment to appease staff and investors and to not appear old-fashioned (whether justified or not).
SPARK has not been around since 1983, only Ada has (there was a SPARK83, but it was not around in 83 but rather based on the Ada 83 standard). SPARK got started as a a second layer on top of Ada through comments processed by a separate tool. SPARK 2014 brought SPARK into more of a first-class status with Ada by being built on a capability that Ada 2012 introduced to the language, aspects.
Rust was not developed to fill the same role as SPARK, anyways. SPARK was developed for design-by-contract and general software correctness. SPARK has only recently been extended to support the memory safety proving that Rust was designed for, and that people find particularly useful.
Rust was not developed to fill the same role as SPARK, anyways. SPARK was developed for design-by-contract and general software correctness. SPARK has only recently been extended to support the memory safety proving that Rust was designed for, and that people find particularly useful.
Everything that ends up being useful was a shiny new thing once. Shiny new things get us excited about the future and motivated to build stuff because they give us hope of solving problems that aren't solved yet.
It's worth pointing out that Rust began as a passion project to try and improve the reliability of systems programming. Given that this is still a huge problem today, you can probably imagine it was an even bigger problem back then and Ada had been around for decades by that point, so clearly it had not solved the problem.
It's worth pointing out that Rust began as a passion project to try and improve the reliability of systems programming. Given that this is still a huge problem today, you can probably imagine it was an even bigger problem back then and Ada had been around for decades by that point, so clearly it had not solved the problem.
When Ada/SPARK have been around since 1983, then what was the reason for inventing Rust?
Rust was more inspired to be a memory safe, C++ like language, with a better syntax and type system. It’s far more targeted towards application programming than anything else, although it’s looking better and better for embedded as well. Although it can probably be used for safety critical applications in the future, it’ll need better tooling before that can happen.
Anyway, the primary issue with Ada/SPARK in the (F)OSS ecosystem is primarily due to the lack of available compilers IMO. On top of that it has a reputation as a somewhat “dead” language and, as silly as it is, many people can’t bring themselves to look past the pascal style syntax. That said, Ada/SPARK is not the only game in town. JML exists for Java, Frama-C and Astrée can basically offer equivalent functionality, and I’m sure others exist (ployspace code prover?). So you might as well ask “why Ada/SPARK?”.
Why does our industry get so enthused with shiny new things, repetitively?
Personally I believe that Rust appeals to many who have historically avoided native development because C and C++ are just such a bother to deal with. It’s hard to imagine Rust being where it is today without cargo. Now, with security only becoming more of a serious problem, Rust is becoming more compelling for some users.
Rust was more inspired to be a memory safe, C++ like language, with a better syntax and type system. It’s far more targeted towards application programming than anything else, although it’s looking better and better for embedded as well. Although it can probably be used for safety critical applications in the future, it’ll need better tooling before that can happen.
Anyway, the primary issue with Ada/SPARK in the (F)OSS ecosystem is primarily due to the lack of available compilers IMO. On top of that it has a reputation as a somewhat “dead” language and, as silly as it is, many people can’t bring themselves to look past the pascal style syntax. That said, Ada/SPARK is not the only game in town. JML exists for Java, Frama-C and Astrée can basically offer equivalent functionality, and I’m sure others exist (ployspace code prover?). So you might as well ask “why Ada/SPARK?”.
Why does our industry get so enthused with shiny new things, repetitively?
Personally I believe that Rust appeals to many who have historically avoided native development because C and C++ are just such a bother to deal with. It’s hard to imagine Rust being where it is today without cargo. Now, with security only becoming more of a serious problem, Rust is becoming more compelling for some users.
Given that the recent downtime of the U.K. air traffic control system, implemented in ADA Spark by the way ... was triggered by a straightforward flight plan with two duplicate exit points...Maybe the competence of individuals, teams, and quality control measures has a more pronounced influence.
Also...GNAT Pro for Rust: https://www.adacore.com/press/adacore-announces-gnat-pro-for...?
Also...GNAT Pro for Rust: https://www.adacore.com/press/adacore-announces-gnat-pro-for...?
> implemented in ADA Spark by the way
The corresponding subsystem by Frequentis AG is implemented in Java. And apparently halting the system in case of wrong/unexpected flightplan data was a "feature"; according to the investigation report this has been changed now (see https://news.ycombinator.com/item?id=37401864). Even with Rust there is still the problem of misconceptions in analysis or specifications, or of wrong design decisions.
The corresponding subsystem by Frequentis AG is implemented in Java. And apparently halting the system in case of wrong/unexpected flightplan data was a "feature"; according to the investigation report this has been changed now (see https://news.ycombinator.com/item?id=37401864). Even with Rust there is still the problem of misconceptions in analysis or specifications, or of wrong design decisions.
Doesn't seem like a good faith question because you've already made your conclusion with the second part.
Ada job postings usually come with a "Security clearance required", less so with Rust.
Because new?
Because short / terse / expressive
Because C like
Because short / terse / expressive
Because C like
Why does our industry get so enthused with shiny new things, repetitively?