5 ms·
If people cared about correctness, they would use CompCert instead of GCC or Clang.
by qznc 6y ago
If people cared about correctness, they would use CompCert instead of GCC or Clang.
- tobylane 6y agoCompCert doesn’t guarantee these two functions will work. Thanks, didn’t know about that project.
- pjmlp 6y agoOr create OSes where applications are all written in managed languages, and the use of GCC and clang is gate keeped to the OS vendor and native libraries, just an idea.
- MaxBarraclough 6y agoBit of a nitpick, but the real value is in safe languages, rather than managed languages, no? The distinction is a little blurry, admittedly, but as an example, I figure that verified SPARK counts as safe but unmanaged.
- pjmlp 6y agoBecause as you might have guessed, I was speaking of iOS, Android and ChromeOS, while SPARK as much as I like it, is a very niche technology.
- MaxBarraclough 6y agoI should have gone with a less niche example: the safe subset of Rust. D also has a safe subset.
- pjmlp 6y agoStill niche, Rust is not up to the stuff that app developers expect in terms of tooling and D still has quite a few @safe bugs to sort out, among its current adoption issues. Unfortunely regardless of their own reports regarding CVEs, Microsoft, Apple and Google keep turning to C and C++ for their bottom layers + managed languages, instead of going full speed in some of those alternatives. So it appears to be the long term solution to mitigate security issues, while keeping compatibility with existing code and tooling.
- eru 6y agoWhy use managed languages when you can prove your code correct?
- pjmlp 6y agoWith what, Frama-C? Good luck getting it adopted outside domains that enforce its use for code certification.
- eru 6y agoFrama-C is a specific compiler. It has not much to do with proving your own code. (And C ain't a good language for writing code you want to prove correct in.) You are right that after having proven your code correct, you might want to use an implementation (compiler or interpreter), that is also proven correct. But those are still two different things.
- dhekir 6y agoFrama-C is a framework for code analysis. It can help proving code with the aid of ACSL (JML-like notation for C contracts). But I agree that C is not the best language for writing critical code.