I'll admit I don't know much about Ada, but the "when" syntax additions described here look interesting. Is there any difference between "return when ..." and "if ...: return" in Ada?
Wow, my first “real world” programming language. Heavily used in critical systems software. Our company worked on aircraft controls and Ada was pretty much the only one “approved” by the regulators as I understood it back then. Anyone working on it currently can speak to if it’s still widely used and what this change means for Ada?
I really hope that’s inaccurate. As much as I love programming in c++, I find it very hard to believe that the same number of nines can be achieved as Ada for similar budget.
Oh don't worry, the F-35 is already a twisted vanity project of the military industrial complex largely created to siphon off as many percentage points of the US budget as possible. The goal is not nines, it's getting more executives out on the field to play Nines*.
C/C++ is used over Ada just for familiar syntax. From a safety perspective, the choice of language is inconsequential. With C/C++ the code analyzers used must do more work than with Ada but not that much.
All safety-critical code uses just a tiny subset of the language. It's like programming in a different language. Line-by-line coder reviews are a must.
The linked PDF doesn't seem to mention anything related specifically to C++. It says that it is possible for bit flips to affect software. They then suggest that Toyota should have used the following practices:
• “Near-perfect” software
• Design out single points of failure
• Justify real time scheduling with analysis
• Watchdog timers that have real “bite”
• Good software architecture
• Good safety culture
This seems like mostly good concrete advice, although I think we can all agree that simply creating "near-perfect software" is a goal, not a solution. If you read up on Toyota's unintended breaking legal issues, it appears that it was most likely driver error, as Toyota did not issue a firmware change to the affected vehicles, and no software problems were ever identified.
> From a safety perspective, the choice of language is inconsequential.
Citation very much needed. Some safety-critical projects choose to use Ada over C or C++, despite that there are far fewer Ada programmers out there, and that there are fewer development tools for Ada. The people running those projects presumably disagree with you.
We know that the choice of language is very consequential regarding cybersecurity. The many foot-guns of C and C++ are the root of a significant fraction of security vulnerabilities. Saying that these same foot-guns are of no consequence in safety-critical software seems like a remarkable claim.
This document [0] explicitly disagrees with your position that language is of little consequence. (Not to gloss over that it appears to have been funded by AdaCore, who are of course motivated to reach that conclusion.)
> C/C++ is used over Ada just for familiar syntax. From a safety perspective, the choice of language is inconsequential. With C/C++ the code analyzers used must do more work than with Ada but not that much.
That is completely and utterly false despite the millions (billions ?) invested in trying to make sound & safe static analysis tools for C/C++. I know you're trying to push that message but it couldn't be further from the truth. The nature of C & C++ is such that you cannot avoid unsafety, even with very restricted subsets.
Disclaimer: I work on Ada tools, but have also worked on C/C++ tools. I have also studied MISRA C and worked on such static analyzers for C & C++.
A non-trivial part of the problems is related to non-flying software, ALIS (now renamed ODIN, when the contract to redo it was awarded to the same people who fucked it up first).
Knowing Lockheed-Martin, it's horrible mess of Java and JavaScript gathered from random geocities pages in 1990s.
C/C++ is used over Ada just for familiar syntax. The coding standards used for safety-critical projects limit the features into a tiny safe subset, Essentially DSL.
Linters and code checkers and static analyzers check the code more thoroughly than the compiler does.
For example, all memory is allocated during initialization. No allocation or reallocation from the heap afterward. That's why you see in the weapon specs familiar magic numbers like can track 256 targets simultaneously.
JOINT STRIKE FIGHTER AIR VEHICLE C++ CODING STANDARDS FOR THE SYSTEM DEVELOPMENT AND DEMONSTRATION PROGRAMDocument Number2RDU00001 Rev C December 2005
https://www.stroustrup.com/JSF-AV-rules.pdf
Ada and C++ are worlds apart, how is it possible to come so close as to be "just syntax" with static analyzers and their known limitations? Unless we are talking about all programming languages being "just syntax" for a turing machine...
More importantly the workforce is familiar with C/C++, how it’s listed on so many job listings. Which is kind of sad as a requirement. A programmer who can’t become productive with Ada after a few weeks (productive, not masterful) is not the kind of programmer anyone should be hiring for any job. The syntax is (almost) dead simple, for a reason.
Those jobs require competence from most contributors. Mastery from a few. And you can teach mastery to non-incompetent people, most of the time. Also, most jobs that Ada would be used for aren't time critical (in the sense of "Oh god oh god oh god we've got to ship yesterday!", unless it's F-35, which fortunately didn't use Ada because that would've saved them a lot of heartache). They program in 2-5 years for the project so 1 month to competency and then additional OJT from more experienced (with Ada and the system) over the rest of the time will produce mastery.
Yes. But as I said, programmers use just tiny subset of the language. Subsets are with additional checks are semantically very similar. Very dumped down code.
> being "just syntax" for a turing machine..
If you insist, I would describe them as intermediate representations for the back-ends for a non-Turing equivalent language (after all semantic checking).
Compilers parse text, check it matches the syntax, do some semantic checks, and then output native code (unless they transpile). When you write safety-critical code you can buy tools that make more far more checks to the semantics than the compiler and prevent the use of some constructs. Ada has SPARK that is integrated better.
For example, the tool I mention can prove that if code has no run-time errors or divisions by zero. It's essentially non-Turing equivalent language.
I would prefer Ada/Spark over C, but it don't matter that much, so I have always used C with tooling.
As said in another comment, that's completely and demonstrably false.
As soon as a coding standard for C/C++ doesn't completely forbid the use of pointers (which is completely impossible at least in C), then it will be much more unsafe than Ada (or other alternatives like Rust).
You can have - very painfully - near pointer free programming in C++, but it requires the use of high level constructs (smart pointers, RAII, etc) that most if not all safety critical standards forbid the use of.
Some people like the Frama-C people are trying to make programming in - a restricted an enhanced subset of - C, safe. They're basically doing Ada/SPARK with annotations in C, and it's horribly painful.
So, despite its informed and documented appearances, your comments are spreading misinformation about what it's like to program in C/C++ for safety critical systems.
Astrée static analysis tool detects invalid pointer dereferences. It can give false alarms but it always detects errors. It does this buy using abstract interpretation on the semantics. It's essentially partial execution.
Here's a very telling quote regarding the choice of programming language from a software team manager from the JSF project:
"Ada was seen as the technically superior and more robust language, but concern over the ability to successfully staff the software engineers required to develop the massive amounts of safety critical software caused the F-35 team to carefully look and finally to choose C and C++ for the implementation of safety critical software." - John H. Robb, Senior Manager of the F-35 Joint Strike Fighter Air Vehicle Software team at Lockheed Martin Aeronautics Fort Worth[1]
Probably a good analogy for the languages too. One tries to do one thing well, the other tries be all things to all users and does them all mediocrely.
Ada is really in a bad place. It’s too generalist for safety critical applications. A DSL is a much better fit, restricting operations and possible side effects to a minimum. At the same time, it’s very abstract and somewhat esoteric, meaning capable developers and tools are hard to find. Everywhere I look it is replaced by something else.
> It’s too generalist for safety critical applications. A DSL is a much better fit, restricting operations and possible side effects to a minimum.
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.
C and C++ were not designed with critical applications in mind. Therefore you cannot apply the same criticism to them.
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.
Your point is wrong. C was /not/ intended for safety critical applications. Therefore, it makes sense that using it in that context will require adaptation.
On the contrary my dear, Ada has been usable for 30 years before SPARK came to be, SPARK only makes it better by adding features that usually are only found in languages like Idris and Coq.
SPARK is something I wish all languages were: formally provable as a first class citizen. I'm interested in changing from C++ to SPARK, but ADA without SPARK isn't really interesting to me. Of course I work on an application that can kill people, and we are planning on eliminating some of the human safety checks if we can convince ourselves that we won't kill people without them.
> SPARK is something I wish all languages were: formally provable as a first class citizen.
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.
Ada was not designed for formal verification. It was designed to build safety-critical software and to standardize and unify the US Department of Defense's panoply of programming languages.
"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."
>> 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.
> 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.
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.
> You do realize that there can’t be a Turing-complete language that can be formally verified?
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.
Fortunately I don't care about the halting problem in the general case. I run code that shouldn't halt (except when the power turns off). I need the basic algorithms to finish, which is a variation on halting, but I can restrict the input such that my case of the halting problem is no longer the general case you can't solve.
> If you have to restrict the language to attain the goal of the language, that’s a bad place to be.
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).
> 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.
In fairness, the existence of unsafe Rust means that Rust as a whole isn't safe by construction. Rust's safety system does a great job of isolating especially risky code from safe(r) code. 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. 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.
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.
> the existence of unsafe Rust means that Rust as a whole isn't safe by construction
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.)
I've read the book on ada language recently and it looked interesting, but the developer experience is a mess. IDE that' s provided got kicked out from ubuntu repositories due to complicated build process. Language server is there, but there is not much documentation in the wild and the community is quite small and the whole situation with gpl compiler affecting compiled programs is poisoning.
I think ada as a language is in a very similar place to common lisp - there are few commercial vendors (one in case of ada) that sell compiler(s) and support to companies with a lot of existing code, but not much new stuff happening apart from few enthusiasts.
Ada is mostly used by professionals, not enthusiasts. It has a captive audience of governments and companies working on safety-critical systems where they have strict toolchain requirements or legacy systems. Pretty much the only thing that can move those users off Ada is to retire older systems, and rebuild their processes for C++. That's tough to justify when the language and ecosystem are still actively developed (paid, not free tools). Things like a language server are unimportant when your IDE must be qualified, and you're not allowed to install or use any software of your choosing. You will never see most of what goes on with Ada outside of a work environment. Its continued use is largely unaffected by anything you'd see in the open source community.
Ada was released in 1980. It finally got a free compiler when the Air Force paid for one in 1995 fifteen years later and it took until 2001 for this code to finally be merged with the rest of GCC.
It definitely had no free compiler for a long time.
That it took 16 years to develop a free compiler for a relatively niche language in the era when relatively few people were online yet in any meaningful sense is not terribly shocking.
The language, going with the date of the first spec, is now 41 years old. So 25 years of its existence, there has been a free compiler. Quite a bit longer than the time spent without one.
That's not at all what I'm saying. Aside from web development, most professional tools are only used by professionals because they cost money. It wouldn't make sense to judge something by the free toy versions that happen to exist.
You can label your loops and use an inner labeled single-pass loop, you can have labels such as "<<Continue>>" to what you can do a "goto Continue", or you can raise an exception that does "null", which does nothing and carries on to the next iteration.
There is a curious parallel with the Ada vs. C/C++ thing in the HDL world: VHDL uses Ada-like syntax, whereas Verilog, C-like. (Looks like mostly a matter of taste.)
69 comments
[ 2.4 ms ] story [ 75.2 ms ] threadThis, together with the `@` syntax, are interesting cases of adding a bit more sugar to Ada. Hopefully it heralds a good future.
* Niche golf game.
C/C++ is used over Ada just for familiar syntax. From a safety perspective, the choice of language is inconsequential. With C/C++ the code analyzers used must do more work than with Ada but not that much.
All safety-critical code uses just a tiny subset of the language. It's like programming in a different language. Line-by-line coder reviews are a must.
https://users.ece.cmu.edu/~koopman/pubs/koopman14_toyota_ua_...
• “Near-perfect” software
• Design out single points of failure
• Justify real time scheduling with analysis
• Watchdog timers that have real “bite”
• Good software architecture
• Good safety culture
This seems like mostly good concrete advice, although I think we can all agree that simply creating "near-perfect software" is a goal, not a solution. If you read up on Toyota's unintended breaking legal issues, it appears that it was most likely driver error, as Toyota did not issue a firmware change to the affected vehicles, and no software problems were ever identified.
Citation very much needed. Some safety-critical projects choose to use Ada over C or C++, despite that there are far fewer Ada programmers out there, and that there are fewer development tools for Ada. The people running those projects presumably disagree with you.
We know that the choice of language is very consequential regarding cybersecurity. The many foot-guns of C and C++ are the root of a significant fraction of security vulnerabilities. Saying that these same foot-guns are of no consequence in safety-critical software seems like a remarkable claim.
This document [0] explicitly disagrees with your position that language is of little consequence. (Not to gloss over that it appears to have been funded by AdaCore, who are of course motivated to reach that conclusion.)
[0] See especially page 12: (PDF) https://www.adacore.com/uploads/techPapers/Controlling-Costs...
That is completely and utterly false despite the millions (billions ?) invested in trying to make sound & safe static analysis tools for C/C++. I know you're trying to push that message but it couldn't be further from the truth. The nature of C & C++ is such that you cannot avoid unsafety, even with very restricted subsets.
Disclaimer: I work on Ada tools, but have also worked on C/C++ tools. I have also studied MISRA C and worked on such static analyzers for C & C++.
Knowing Lockheed-Martin, it's horrible mess of Java and JavaScript gathered from random geocities pages in 1990s.
well, it fits that the F-35 started as a horrible mess of JSF requirements bolted on top of Yak-141 from 1980s :)
C/C++ is used over Ada just for familiar syntax. The coding standards used for safety-critical projects limit the features into a tiny safe subset, Essentially DSL. Linters and code checkers and static analyzers check the code more thoroughly than the compiler does.
For example, all memory is allocated during initialization. No allocation or reallocation from the heap afterward. That's why you see in the weapon specs familiar magic numbers like can track 256 targets simultaneously.
Commerical code analyzers used in the military, aviation, etc. are good but expensive. I have used https://www.absint.com/astree/index.htm
JOINT STRIKE FIGHTER AIR VEHICLE C++ CODING STANDARDS FOR THE SYSTEM DEVELOPMENT AND DEMONSTRATION PROGRAMDocument Number2RDU00001 Rev C December 2005 https://www.stroustrup.com/JSF-AV-rules.pdf
Yes. But as I said, programmers use just tiny subset of the language. Subsets are with additional checks are semantically very similar. Very dumped down code.
> being "just syntax" for a turing machine..
If you insist, I would describe them as intermediate representations for the back-ends for a non-Turing equivalent language (after all semantic checking).
Compilers parse text, check it matches the syntax, do some semantic checks, and then output native code (unless they transpile). When you write safety-critical code you can buy tools that make more far more checks to the semantics than the compiler and prevent the use of some constructs. Ada has SPARK that is integrated better.
For example, the tool I mention can prove that if code has no run-time errors or divisions by zero. It's essentially non-Turing equivalent language.
I would prefer Ada/Spark over C, but it don't matter that much, so I have always used C with tooling.
I don't know what they've done, but you could get a long way just by forbidding all dynamic allocation.
As soon as a coding standard for C/C++ doesn't completely forbid the use of pointers (which is completely impossible at least in C), then it will be much more unsafe than Ada (or other alternatives like Rust).
You can have - very painfully - near pointer free programming in C++, but it requires the use of high level constructs (smart pointers, RAII, etc) that most if not all safety critical standards forbid the use of.
Some people like the Frama-C people are trying to make programming in - a restricted an enhanced subset of - C, safe. They're basically doing Ada/SPARK with annotations in C, and it's horribly painful.
So, despite its informed and documented appearances, your comments are spreading misinformation about what it's like to program in C/C++ for safety critical systems.
"Ada was seen as the technically superior and more robust language, but concern over the ability to successfully staff the software engineers required to develop the massive amounts of safety critical software caused the F-35 team to carefully look and finally to choose C and C++ for the implementation of safety critical software." - John H. Robb, Senior Manager of the F-35 Joint Strike Fighter Air Vehicle Software team at Lockheed Martin Aeronautics Fort Worth[1]
[1]https://web.archive.org/web/20111219004314/http://journal.th...
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]
[0] http://archive.adaic.com/projects/atwork/boeing.html
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
I think ada as a language is in a very similar place to common lisp - there are few commercial vendors (one in case of ada) that sell compiler(s) and support to companies with a lot of existing code, but not much new stuff happening apart from few enthusiasts.
=It's just my anecdotal experience tough.
https://www.adacore.com/
https://www.ghs.com/products/ada_optimizing_compilers.html
https://www.ptc.com/en/products/developer-tools/apexada
https://www.ddci.com/products_score/
http://www.irvine.com/tech.html
http://www.ocsystems.com/w/index.php/OCS:PowerAda
http://www.rrsoftware.com/html/prodinf/janus95/j-ada95.htm
A polite way of saying it's rarely used willingly.
Overall, it's a pretty nice language.
It definitely had no free compiler for a long time.
The language, going with the date of the first spec, is now 41 years old. So 25 years of its existence, there has been a free compiler. Quite a bit longer than the time spent without one.