[zozbot234]

> I've never read anything to make me think that Rust is a safer alternative than any of these options

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.

[johnisgood]

So what is the issue with Ada/SPARK?

[jerf]

I can't think of a case of a system like that being revived after 10 or more years. My best guess is that the mismatch between the environment the language was written in and the modern world simply becomes too great for anyone to care after a while.

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.

[grumblenum]

Why are you using past tense for Ada? Adacore is still doing business and Ada 202x will be standardized this year or next.

I’m also not sure why “nice JSON libraries” is a hard requirement for kernel code. Also, see JWX.

[jerf]

Why past tense? Because it's dead as languages go. Defining "death" as "zero users" is not the definition most people use, because it's not useful; things are clearly dead before that point. Ada doesn't have a bright future. It isn't going to rise from the ashes and have everyone agree that yes, it was right all along, and everybody with 10 years of experience on their resume is suddenly in hot demand as the crowds give them ticker tape parades for having been right all along. That never happens. It may well klunk along for more decades... but it's dead.

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

[ajxs]

Ada should be considered dead because it doesn't have an npm full of super[1] useful[2] libraries?

> 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

[2] https://www.npmjs.com/package/is-array

[3] https://www.adacore.com/company/our-customers

[johnisgood]

> Ada should be considered dead because it doesn't have an npm full of super[1] useful[2] libraries?

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

[1] https://alire.ada.dev/

[2] https://blog.adacore.com/first-beta-release-of-alire-the-pac...

[grumblenum]

So dead "because I said so" in essence?

[spicybright]

Very few users over a long period of time means very few are working to keep the language up to date.

Too long of this pattern and it becomes much more trouble than it's worth to use on a business level.

[Dylan16807]

No more than you're saying it's not dead "because I said so".

They gave a bunch of reasons.

[tome]

Not sure what you mean about Haskell. Haskell is seeing more activity than it has even seen!

[livinginfear]

What kind of scalable approach are you describing? Rust is not formally verifiable. I'm aware that there are projects attempting to solve this problem, however as I understand it you can't currently create verifiable production code.

[grumblenum]

> focusing purely on type- and memory-safety, not conformance to arbitrary specifications

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?

[zozbot234]

Types are not 'arbitrary' in any real sense. Type systems can be described as a sort of formal verification that leverages and is closely aligned with the syntax structure of actual code, thus type systems can preserve compositionality but don't generally support non-local reasoning, at least not in a very elegant way. This is exactly what can make them potentially more scalable than other sorts of FV, hence more useful for programming "in the large".

[grumblenum]

Types that can be defined by users are, necessarily, part of a language syntax, so that they are aligned with the syntax is just a tautology. Equating user defined types with formal verification is just nonsense. C has types. Python has types. Rust has types. That the program does what you think it should do does not logically follow the mere existence of types. I have no idea what "in the large" is supposed to mean. I feel like GPT-3 is arguing with me.

[PhaseLockk]

Maybe I can try to explain the parent comment's point a different way. When saying that rust works on types and not on arbitrary specifications, I think he is saying that rust is more limited than languages that support arbitrary specifications. However, by making this tradeoff it achieves a reasonable degree of safety without incurring a ton of overhead.

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.

[marshray]

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

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

[wtetzner]

I believe what zozbot234 is saying is that Rust focuses on a specific subset of formal verification, and on trying to make a language with that enforces that subset in a way that is still somewhat ergonomic.

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.