Comment by AlotOfReading
2 days ago
SAW/Cryptol are amazingly easy to use compared to other formal methods tools. It's a shame that C++ is still popular in high assurance spaces, because the tooling for it and the ability to write safe code is so much worse than C these days.
When did C got safe strings and arrays?
Ideally neither C nor C++ should be used when security matters.
Explain to someone like me who uses C in safety-critical software in aerospace and defense why not?
For me, choosing the language is not enough. It's the tooling that goes far beyond the language that is important for safety and quality of compiler and runtime. C has very mature tooling options. So does ADA.
https://www.absint.com/astree/index.htm
Abstract Interpretation in a Nutshell https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
Explain to us why you are not allowed to use 100% of ISO C, without certification processes that castrate C to the point it feels like Ada 83 with curly brackets.
Proceses that outside high integrity computing no one is willing to make themselves go through without legal requirements and liability.
Most of it because during 1980's it was cheaper to advocate for C plus certification than pay for Ada compilers and developers.
5 replies →
I've never met a company I could convince to buy an Ada toolchain. Someone at Nvidia managed the feat and it's a pretty good measure of their enthusiasm that they seem to be pushing the hard work off onto adacore instead of spreading it internally.