5 ms·

Would it make you feel better if I told you that these kinds of offerings usually also don't offer modern validation tools like sanitizers? They expect people t

Would it make you feel better if I told you that these kinds of offerings usually also don't offer modern validation tools like sanitizers? They expect people to just wing it with whatever the proprietary IDE happens to give them. A big part of the job of safety critical development is knowing the difference between box checking best practices/regulations and building actually safe systems so you can do both.

yjftsjthsd-h 2y ago
I would assume the solution is to run your code through multiple compilers/toolchains - in dev, CI can run the certified compiler to make sure your code stays compatible with it, but also through modern clang/gcc with every linter and static analysis tool you can think of. Then for the "official" prod builds you use the certified compiler. Automated testing should probably use both, and even compare the behavior of binaries from each chain to look out for bugs that only exist in one. That way you get most of the benefits of both worlds (not all, since you can only write code that all compilers can handle).
- steveklabnik 2y ago
  It isn’t. The idea is to quantify the risk. A buggy toolchain is okay if the bugs are known and you can demonstrate how you’re mitigating them. All software has bugs, you cannot rely on the idea of bug free software to ensure safety, you must have a process that is robust in the face of problems.
  - yjftsjthsd-h 2y ago
    Sure, but if you can do something to reduce the number of bugs it seems like you should still do that?
    - steveklabnik 2y ago
      I don’t disagree that in general, reducing the number of bugs is a good goal, but there’s always a limit to how far you go. It’s not like every line is formally proven, for example. Just because you can use a specific technique doesn’t mean that you must. But also I don’t work directly in these industries and so maybe my impression of this aspect of their processes is incorrect.
      - tialaramex 2y ago
        I actually think far more of these safety of life standards should require formal proof. IMNSHO the standards were set so low so that C++ could clamber over the low bar, and it's a happy consequence in some sense that Rust has no trouble clearing it, but the bar should be raised considerably instead. Software crucial to the safe operation of an airliner ought to be proven correct, not just slapped together in any of the general purpose languages, including Rust and then subject to a bit more process than for a web app.
        adrianN 2y ago
        That would explode the costs for marginal safety improvements. I think the same effort spent on better requirement engineering would yield more payoff.
        tialaramex 2y ago
        Why do you believe this would "explode the costs" ? Why would the resulting safety improvements be "marginal" ?
        adrianN 2y ago
        Because proving correctness for complex software is difficult and very few people have relevant experience. So it is both labor intensive and you need to pay high wages. I believe the safety improvements are marginal because of my experience in safety critical development. Almost all the bugs we did not find by testing turned out to be problems with the requirements that led to interoperability issues. Proving the correct implementation of wrong requirements would not have helped.
- AlotOfReading 2y ago
  That's a common partial solution, but it's not complete. For example, it essentially requires you to be able to observe all safety-relevant behaviors of the code in both compilers. This is a much more comprehensive degree of validation than almost any system actually achieves. You also run into issues where the behaviors you're observing (e.g. low bits in floating point results) depend on intimate details of codegen that aren't identical between compilers. The complete solution depends on the application and the integrity level. It's not one size fits all, but rather about producing documentation showing you've considered various failure modes and developed mitigations for them (or otherwise accept the risk). Sometimes that's binary analysis of the compiled output to ensure it meets some formal model, sometimes that's a formally proven, decent compiler like concert, and so on. An additional wrinkle is that the business model for high integrity compilers can also be a huge obstacle here. Some charge seats by how many people have modified the code that's running through the compiler. These aren't cheap licenses either, so companies have a large incentive not to use methodologies that require many eyes making all bugs shallow. There are also issues running these compilers in CI. They might require online license verification on every file, for example, or not allow ephemeral licensing at all.

yjftsjthsd-h 2y ago

I would assume the solution is to run your code through multiple compilers/toolchains - in dev, CI can run the certified compiler to make sure your code stays compatible with it, but also through modern clang/gcc with every linter and static analysis tool you can think of. Then for the "official" prod builds you use the certified compiler. Automated testing should probably use both, and even compare the behavior of binaries from each chain to look out for bugs that only exist in one. That way you get most of the benefits of both worlds (not all, since you can only write code that all compilers can handle).

steveklabnik 2y ago
It isn’t. The idea is to quantify the risk. A buggy toolchain is okay if the bugs are known and you can demonstrate how you’re mitigating them. All software has bugs, you cannot rely on the idea of bug free software to ensure safety, you must have a process that is robust in the face of problems.
- yjftsjthsd-h 2y ago
  Sure, but if you can do something to reduce the number of bugs it seems like you should still do that?
  - steveklabnik 2y ago
    I don’t disagree that in general, reducing the number of bugs is a good goal, but there’s always a limit to how far you go. It’s not like every line is formally proven, for example. Just because you can use a specific technique doesn’t mean that you must. But also I don’t work directly in these industries and so maybe my impression of this aspect of their processes is incorrect.
    - tialaramex 2y ago
      I actually think far more of these safety of life standards should require formal proof. IMNSHO the standards were set so low so that C++ could clamber over the low bar, and it's a happy consequence in some sense that Rust has no trouble clearing it, but the bar should be raised considerably instead. Software crucial to the safe operation of an airliner ought to be proven correct, not just slapped together in any of the general purpose languages, including Rust and then subject to a bit more process than for a web app.
      - adrianN 2y ago
        That would explode the costs for marginal safety improvements. I think the same effort spent on better requirement engineering would yield more payoff.
        tialaramex 2y ago
        Why do you believe this would "explode the costs" ? Why would the resulting safety improvements be "marginal" ?
        adrianN 2y ago
        Because proving correctness for complex software is difficult and very few people have relevant experience. So it is both labor intensive and you need to pay high wages. I believe the safety improvements are marginal because of my experience in safety critical development. Almost all the bugs we did not find by testing turned out to be problems with the requirements that led to interoperability issues. Proving the correct implementation of wrong requirements would not have helped.
AlotOfReading 2y ago
That's a common partial solution, but it's not complete. For example, it essentially requires you to be able to observe all safety-relevant behaviors of the code in both compilers. This is a much more comprehensive degree of validation than almost any system actually achieves. You also run into issues where the behaviors you're observing (e.g. low bits in floating point results) depend on intimate details of codegen that aren't identical between compilers. The complete solution depends on the application and the integrity level. It's not one size fits all, but rather about producing documentation showing you've considered various failure modes and developed mitigations for them (or otherwise accept the risk). Sometimes that's binary analysis of the compiled output to ensure it meets some formal model, sometimes that's a formally proven, decent compiler like concert, and so on. An additional wrinkle is that the business model for high integrity compilers can also be a huge obstacle here. Some charge seats by how many people have modified the code that's running through the compiler. These aren't cheap licenses either, so companies have a large incentive not to use methodologies that require many eyes making all bugs shallow. There are also issues running these compilers in CI. They might require online license verification on every file, for example, or not allow ephemeral licensing at all.