That's exactly what Ada's 'SPARK' subset provides. SPARK can be formally verified, which may be valuable for highly critical work.
Also, your criticism applies just as well to C, and even more so to C++, but those languages see plenty of use in safety-critical domains.
> At the same time, it’s very abstract and somewhat esoteric, meaning capable developers and tools are hard to find.
Ada's concepts are not particularly abstract, and are not particularly difficult to learn. A C/C++ programmer should be able to transition to Ada without too much trouble, as it's somewhat different but it's still a statically typed imperative language. It's not like Haskell where you'd need to re-learn the very basics.
Transitioning from C++ to Ada would be less of a leap than transitioning from C++ to, say, JavaScript.
SPARK is a proof that something is wrong. If you have to restrict the language to attain the goal of the language, that’s a bad place to be.
Furthermore, as you have stated, such « safe » subsets can be defined for other languages like C or C++. Once you have that, why struggle hiring or training rare Ada developers?
Both dynamics are bringing Ada adoption to a stop. It may be a shame but that’s what I see.
For Ada it does not. It’s tire patching.
You can write safety-critical code in the full Ada language, but you won't be able to use SPARK's verification tools.
An example: if I understand correctly, the Boeing 777's avionics software is written in Ada, and they did not use the SPARK subset. [0]
It wouldn't make sense for the average language to make this a goal. The cost is steep. To the typical programmer, SPARK looks like a thoroughly anaemic language, which of course it is.
If Rust, say, had made formal verification a goal, it would have had to sacrifice its ergonomics to the point it would lose much of its appeal.
"SPARK is a programming language and a set of verification tools designed to meet the needs of high-assurance software development. SPARK is based on Ada, both subsetting the language to remove features that defy verification and also extending the system of contracts by defining new Ada aspects to support modular, constructive, formal verification."
Source: https://docs.adacore.com/spark2014-docs/html/lrm/introductio...
>> Both dynamics are bringing Ada adoption to a stop. It may be a shame but that’s what I see.
I disagree. The success of Rust as a replacement for C++ has brought a renewed interest to Ada. Rust has many great ideas and many of them are being added to SPARK. Several ideas from Ada will likely be added to Rust as work from Ferrous Systems and others prepares Rust for use in safety-critical domains.
https://fosdem.org/2021/schedule/event/safety_opensource_ada...
You do realize that there can’t be a Turing-complete language that can be formally verified? You either restrict the language, or you will meet the halting problem.
I don’t see why is it problematic to provide a well-defined subset with stricter guarantees while still having the overall language for parts that need the full computational power of Turing machines.
This is mistaken. Formal verification systems of Turing-complete languages are indeed subject to Rice's theorem, [0] but these systems don't make a claim of totality, i.e. they aren't claiming to always be able to prove all the properties which are true of a program.
Further reading on SPARK: [1][2][3].
> I don’t see why is it problematic to provide a well-defined subset with stricter guarantees while still having the overall language for parts that need the full computational power of Turing machines.
If you're going to make use of parts of the Ada language for which there is no formal model, then your solution is at best going to be partially formally verified. That's not necessarily a bad idea, and you can combine formally verified SPARK with unverified Ada code, but it's also possible to write your whole program in verified SPARK. (That's not to say it's easy/cheap to accomplish at scale. Formal development methodologies are notoriously laborious.)
Using a non-Turing-complete subset of Ada for solving certain problems doesn't strike me as a bad idea necessarily, but it's not the route SPARK goes. I'm not an expert but I believe verification of non-Turing-complete languages is an active area of research, although I think these languages tend to have a functional flavour.
[0] https://en.wikipedia.org/wiki/Rice%27s_theorem
[1] https://www.adacore.com/about-spark
[2] https://learn.adacore.com/courses/intro-to-spark/index.html
[3] https://en.wikipedia.org/wiki/SPARK_(programming_language)
As thesuperbigfrog points out, Ada and SPARK have importantly different goals. You may still be right that Ada is too big and complex for its own good, though. C.A.R. Hoare famously criticized Ada for its complexity.
> « safe » subsets can be defined for other languages like C or C++
It's true that Ada is not actually a safe language, but it's far more easily tamed than C/C++.
The term safe subset is a little misleading here, as, practically, you can't just ban C's dangerous constructs and be left with a safe language. Merely making efforts to comply with MISRA C isn't enough to provide a solid assurance of the absence of undefined behaviour, for instance. For that, you need a full-bore formal verification system, akin to that of SPARK. (For example, SPARK's provers check that there's no way a variable can ever be read before being assigned to. If I understand correctly, in the absence of a prover, the SPARK subset of Ada isn't a fully safe language. I'm not entirely certain on that point though.) I don't know if one exists, but in principle a prover could deal with the full C language, rather than just a subset of it.
This is in sharp contrast to Rust, where there really is a subset which is safe 'by construction' (called Safe Rust).
Hoare later softened his criticism, ca. 1987:
http://computer-programming-forum.com/44-ada/3756b23b2f6890d...
> The combination of many complex features into a single language has led to an unfortunate delay in availability of production-quality implementations. But the long wait is coming to an end, and one can look forward to a rapid and widespread improvement in programming practice, both from those who use the language and from those who study its concepts and structures.
We also need to be careful about what we mean by "safe". Rust's definition of safety isn't exotic, but it doesn't cover the gamut of all possible safety concerns.
That's true, and it's a good reason to be very clear about when the Safe Rust subset is all that's been used. Unfortunately it's rare to hear written in Safe Rust, but that's how we ought to refer to code written purely in the safe subset. It should be a point of pride. (Corollary: making needlessly excessive use of Rust's unsafe features, should be a point of shame.)
> We also need to be careful about what we mean by "safe". Rust's definition of safety isn't exotic
Rust does a fine job of defining safety as they use it:
> If all you do is write Safe Rust, you will never have to worry about type-safety or memory-safety. You will never endure a dangling pointer, a use-after-free, or any other kind of Undefined Behavior. [0]
This total absence of undefined behaviour definition sounds about right to me. I think Safe Rust also guarantees against reading indeterminate data from an uninitialized variable, but by the total absence of undefined behaviour criterion, that's not strictly relevant to whether it's safe.
> it doesn't cover the gamut of all possible safety concerns.
Sure, but that's not really what safe language means.
> But to prove whether your unsafe code is, in fact, safe to use -- you're back to formal verification again, or (more typically) code reviews.
At the risk of sounding pedantic, code reviews do not prove anything about unsafe code, they only lower the odds of a defect making it through your process.
> You can (often) avoid the use of unsafe Rust altogether, but then you're using a subset of the language -- roughly like the case with MISRA C.
I'd flip that round though, as you generally shouldn't be using Rust's unsafe features. I'd rather say that in the rare case that you really need it, Rust offers additional unsafe features beyond the Safe Rust language.
Safe Rust is intended to have excellent ergonomics, very much unlike MISRA C. If Rust is doing its job, its unsafe features should seem like inline assembly in C. C programmers don't generally feel constrained by an absence of assembly code in their codebases, as that kind of code just isn't necessary very often.
(Also, MISRA C isn't a truly safe language, for what that's worth. C is not so easily tamed.)
[0] https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html