5 ms·

C++ is impossible to validate formally. Rust inherently guarantees static memory safety in many situations, on the other hand.

lambdaelite 11y ago
Right, which is why a subset of C or C++ (like MISRA) is used for critical applications.
- monocasa 11y ago
  My day job is currently writing embedded high availability code to a slightly modified version of the JSF coding standard (which is itself a modified version of MISRA for C++). There's a lot of safety that Rust would give us on top of C++ with the coding standard's rules, and we're waiting for Rust to simply mature a little.
  - lambdaelite 11y ago
    To me, it seems like in the future Rust could occupy the same niche as Java + RTSJ does presently. I'm just not clear on how or why Rust would be sufficiently better to overcome the track record of Java + RTSJ.
    - monocasa 11y ago
      JITs and interpreters suck for realtime, and there's only so many optimizations that an AOT compiler can do to a Java codebase (hence why JITs ar so prevalent for Java). Pushing all of these verifications into compile time significantly reduces the run time requirements. Honestly I see Rust as (potentially, down the road) being a better, less verbose Ada than a better C++ or Java. You tend to write Rust code much like you would an Ada or VHDL program.
      - lambdaelite 11y ago
        Both JamaicaVM and PERC seem to have favorable requirements when run with AOT compilation, and the JIT compilation didn't seem too onerous either. What problems have you run into? I ask because I'm in the process of spec'ing out a safety critical medical device, and JamaicaVM is the lead candidate at the moment.
mafribe 11y ago
C++ is impossible to validate formally. This is incorrect. Any language with a well-defined semantics (such as a compiler or interpreter) can be validated formally. It may just be too time-consuming for people to bother. For example the operational semantics of C has been implemented formally, e.g. [1]. The same could be done with C++. [1] http://fsl.cs.illinois.edu/index.php/An_Executable_Formal_Semantics_of_C_with_Applications http://fsl.cs.illinois.edu/index.php/An_Executable_Formal_Se...

lambdaelite 11y ago

Right, which is why a subset of C or C++ (like MISRA) is used for critical applications.

monocasa 11y ago
My day job is currently writing embedded high availability code to a slightly modified version of the JSF coding standard (which is itself a modified version of MISRA for C++). There's a lot of safety that Rust would give us on top of C++ with the coding standard's rules, and we're waiting for Rust to simply mature a little.
- lambdaelite 11y ago
  To me, it seems like in the future Rust could occupy the same niche as Java + RTSJ does presently. I'm just not clear on how or why Rust would be sufficiently better to overcome the track record of Java + RTSJ.
  - monocasa 11y ago
    JITs and interpreters suck for realtime, and there's only so many optimizations that an AOT compiler can do to a Java codebase (hence why JITs ar so prevalent for Java). Pushing all of these verifications into compile time significantly reduces the run time requirements. Honestly I see Rust as (potentially, down the road) being a better, less verbose Ada than a better C++ or Java. You tend to write Rust code much like you would an Ada or VHDL program.
    - lambdaelite 11y ago
      Both JamaicaVM and PERC seem to have favorable requirements when run with AOT compilation, and the JIT compilation didn't seem too onerous either. What problems have you run into? I ask because I'm in the process of spec'ing out a safety critical medical device, and JamaicaVM is the lead candidate at the moment.

mafribe 11y ago

C++ is impossible to validate formally. This is incorrect. Any language with a well-defined semantics (such as a compiler or interpreter) can be validated formally. It may just be too time-consuming for people to bother. For example the operational semantics of C has been implemented formally, e.g. [1]. The same could be done with C++. [1] http://fsl.cs.illinois.edu/index.php/An_Executable_Formal_Semantics_of_C_with_Applications http://fsl.cs.illinois.edu/index.php/An_Executable_Formal_Se...