3 ms·

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

> 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.
- MaxBarraclough 5y ago
  > 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.) [0] https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html

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.

MaxBarraclough 5y ago
> 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.) [0] https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html