What Rust focuses on is providing a scalable approach to a limited kind of formal verification - focusing purely on type- and memory-safety, not conformance to arbitrary specifications. The latter is of course being worked on, but type safety and memory safety are table stakes.
For instance, I have to deal with JSON. There's no reason older languages can't deal with JSON, but it'll often be inconvenient as the libraries try to deal with mismatches in the type system or whatever, and it just can't ever be quite as slick as a more modern language written with some partial, vague combination of the fact that JSON exists in mind, together with the sorts of techniques used to implement JSON support in modern languages. Or sometimes it'll just be the dominant library for dealing with it just has an old design that baked bad assumptions in, and since it's the dominant library it's the one everything uses, so I have to deal with that everywhere.
And it's just the death of a thousand of those cuts. "But you can do JSON in my favored language!" Yeah, but it's just not quite as slick. "But we have an HTTP client in this language!" Yeah, but it's just not quite as slick. "But we have GPU support in my favorite language!" Yeah, but it's just not quite as slick. And you've ground all that "not quite as slick" deeply into your language over the decades.
So nobody has any one reason they can point at as to why Ada isn't going come back, or why E isn't going to come back, or why Cyclone isn't going to come back... but the reality is that the sum total of the issues is more than sufficient to prevent it from ever happening, and what's going to happen is a more modern language is going to get the support.
Advocates also try to "defeat in detail", in analogy to the military technique, arguments to the contrary, but the problem is that while that may satisfy the advocate, everyone else is still left looking at a metaphorical battlefield that has an exhausting number of "battles" over basic deficiencies, and being "defeated in detail" by an advocate just transfers to exhaustion with the underlying language anyhow.
It probably isn't a "the issue" with Ada/SPARK. It's a horde of small little things, the sum total of which is too much hassle for anyone to want to deal with.
I’m also not sure why “nice JSON libraries” is a hard requirement for kernel code. Also, see JWX.
What does happen with such languages is that someone comes along and creates some sort of new language taking the best of the old language and mixing it with more modern stuff. I personally think there's an Ada-like niche waiting to be exploited there, probably something that also takes some lessons from Haskell. (Haskell is still alive, but IMHO, headed toward this sort of dead right now, and really could use this sort of revival itself.) An example of this is Elixir... Erlang would probably be also something I'd be calling "dead" if it weren't for Elixir.
(Ironically, often the biggest partisans of the base language are the last to know about the revival language because every deviation from the base language is seen as a flaw from the One True Answer....)
Too long of this pattern and it becomes much more trouble than it's worth to use on a business level.
They gave a bunch of reasons.
Now, I know that there is a trendy view of "the more the better", and it does not have as many libraries there, but that has to do with the fact that it is not yet widespread among Ada users. Alire is really new.
> That never happens. It may well klunk along for more decades... but it's dead
Ada is used in 2021 in the exact same places that Ada was used in 2011 (and 2001 before it), if not more. Ada was designed for a specific purpose, one that it still fulfills very well. People have been claiming Ada was dead for decades, yet still it miraculously lives on. Despite Rust, despite Haskell, despite an algal bloom of "formally verifiable subsets of C", and so on.
> What does happen with such languages is that someone comes along and...
Yet... This just... hasn't happened. A successor language more suitable for safety-critical development has just simply not appeared. The manufacturers using Ada —a subset of which can be seen at this[3] link— ostensibly don't seem convinced that any of Ada's many alternatives offer a more appropriate solution for developing safety-critical software.
> I personally think there's an Ada-like niche waiting to be exploited...
The Ada-like niche you describe is, believe it or not, currently occupied by Ada. Ridiculous as this may sound, Ada is actually pretty good at fulfilling its intended function. What needs to change? Ada is not designed to fill the role of Node.js, Java, or C#. It's designed for safety-critical embedded systems, which is where you're most likely to find it today.
> Ironically, often the biggest partisans of the base language are the last to know about the revival language because every deviation from the base language is seen as a flaw from the One True Answer...
Does this apply to your thinking too, or just the proponents of Ada, and other languages you don't like? Are the Rust users just blind to the benefits of Ada? Are you susceptible to the same cognitive blind-spot you accuse us of having?
[1] https://www.npmjs.com/package/pad-left
Wait! There is Alire[1][2]! There is a list of "crates", you can easily include them into your project, and so forth. This is pretty much the same as https://crates.io or https://pkg.go.dev, which means people really should throw their misconceptions away and actually do some research before concluding that the language (Ada) is dead. A couple of quick searches quickly tells me that Ada is pretty much alive, with all of these "modern libraries with modern solutions", and full-on safety without performance loss.
This comment is intended for the person you replied to. :)
[2] https://blog.adacore.com/first-beta-release-of-alire-the-pac...
What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?
I believe the comment that types are aligned with the syntax is meant as a contrast to other languages which include specifications written in a format substantially different from or fully removed from the implementation. This can reduce the friction of using type-based verification when compared to formal verification capable of describing an arbitrarily complicated spec.
When discussing the scalability of types, I think he is saying that because types are coupled to the implementation, and don't support non-local reasoning, it is less likely that you will run into issues with type checking as you try to compose many small components into a larger program. In contrast, my impression is that with full formal verification, it can become extremely difficult to properly verify a large system.
Regarding your comparison to C and python, I think it's clear that the parent was comparing the specific type system and borrow checker that Rust provides vs. formal verification, not making a statement about the general concept of a type system. In particular, I don't think it's reasonable to assume he was saying the existence of types provides any sort of safety. Rather, it's clear he was saying the use of a powerful type system (such as that found in Rust or Haskell) to implement a limited specification of the program functionality can provide a degree of safety.
"In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.
If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."
I'm assuming "scalable" in this case is referring to the fact that fully verifying a piece of software is currently takes a large amount of effort. Rust's approach is more "scalable" in the sense that they decided to focus primarily on memory safety, and punted on other forms of verification in the hope that it would be more ergonomic/require less effort.