4 ms·

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

by crocal 5y ago

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.

pjmlp 5y ago
So SPARK is a proof that something is wrong with Ada, while MISRA-C and Frama-C are adaptations?
- sigzero 5y ago
  Pretty much every language could fall into the "something is wrong" category. It's a silly argument.
  - pjmlp 5y ago
    Indeed, that was my point.
    - crocal 5y ago
      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. For Ada it does not. It’s tire patching.
      - MaxBarraclough 5y ago
        Ada and SPARK are not aiming for the same thing. SPARK is intended for formal verification. Ada is not. 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 http://archive.adaic.com/projects/atwork/boeing.html
      - pjmlp 5y ago
        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.
bluGill 5y ago
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.
- MaxBarraclough 5y ago
  > 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.
thesuperbigfrog 5y ago
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." Source: https://docs.adacore.com/spark2014-docs/html/lrm/introduction.html 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.
- pjmlp 5y ago
  Actually it goes both ways, SPARK is adding a kind of borrow checker. https://fosdem.org/2021/schedule/event/safety_opensource_ada_heap_manipulation/ https://fosdem.org/2021/schedule/event/safety_opensource_ada...
kaba0 5y ago
> 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.
- MaxBarraclough 5y ago
  > 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. [0] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem [1] https://www.adacore.com/about-spark https://www.adacore.com/about-spark [2] https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html [3] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
- bluGill 5y ago
  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.
MaxBarraclough 5y ago
> 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).
- gmfawcett 5y ago
  > C.A.R. Hoare famously criticized Ada for its complexity. Hoare later softened his criticism, ca. 1987: http://computer-programming-forum.com/44-ada/3756b23b2f6890d4.htm 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.
- gmfawcett 5y ago
  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.

by crocal 5y ago

pjmlp 5y ago

So SPARK is a proof that something is wrong with Ada, while MISRA-C and Frama-C are adaptations?

sigzero 5y ago
Pretty much every language could fall into the "something is wrong" category. It's a silly argument.
- pjmlp 5y ago
  Indeed, that was my point.
  - crocal 5y ago
    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. For Ada it does not. It’s tire patching.
    - MaxBarraclough 5y ago
      Ada and SPARK are not aiming for the same thing. SPARK is intended for formal verification. Ada is not. 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 http://archive.adaic.com/projects/atwork/boeing.html
    - pjmlp 5y ago
      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.

bluGill 5y ago

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.

MaxBarraclough 5y ago
> 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.

thesuperbigfrog 5y ago

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." Source: https://docs.adacore.com/spark2014-docs/html/lrm/introduction.html 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.

pjmlp 5y ago
Actually it goes both ways, SPARK is adding a kind of borrow checker. https://fosdem.org/2021/schedule/event/safety_opensource_ada_heap_manipulation/ https://fosdem.org/2021/schedule/event/safety_opensource_ada...

kaba0 5y ago

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

MaxBarraclough 5y ago
> 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. [0] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem [1] https://www.adacore.com/about-spark https://www.adacore.com/about-spark [2] https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html [3] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
bluGill 5y ago
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.

MaxBarraclough 5y ago

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

gmfawcett 5y ago
> C.A.R. Hoare famously criticized Ada for its complexity. Hoare later softened his criticism, ca. 1987: http://computer-programming-forum.com/44-ada/3756b23b2f6890d4.htm 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.
gmfawcett 5y ago
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.