4 ms·

My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is form

by nequo 2y ago

My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is formally verified to preserve the intended semantics. So CompCert seems to me to aim to help mission-critical software to move away from C, and possibly into Coq/Isabelle/etc., except for the purposes of compilation to machine code.

lisper 2y ago
That is a noble goal, but I don't see how it can possibly achieve the intended result as long as the C standard is a fundamentally borken as it is. I tried to download CompCert so I could try it out, but they only have a source distribution and to build it you need Coq and OCaml and a few other things because of course CompCert is not written in C. No one in their right mind would write mission-critical software in C.
- seabird 2y ago
  If your original source is provably transpilable to C with no UB, and your compiler provably compiles that C without any bungling, then you've made it. The standard is bad and I want to see the end of C before I'm dead, but this isn't a stretch, and C is just a detail in the process.
- LeFantome 2y ago
  I am mostly in the other side of this argument. C is an insane language in my view ( in a modern context ). That said, what “mission critical software” are you using that is not running on an OS written in C?
  - eru 2y ago
    > > No one in their right mind would write mission-critical software in C. > That said, what “mission critical software” are you using that is not running on an OS written in C? I'm not sure that's relevant? If you have a piece of mission critical software, almost all the time you run it on an existing OS like Windows or Linux. You don't _write_ a new OS just for your one piece of software. Of course, that OS had to be written at some point in the past (and is still being worked on). Presumably that writing was (and is) being done by people not 'in their right mind'. But that shouldn't concern you. The problem with C is not that you can't write secure-ish software at all; the problem is that this is insanely difficult, and that the trade-offs aren't worth it. Especially for new software. For software that I get from some third-party, like the OS, I only care about its quality (and price); I don't care about the trade-offs and pains the authors had to endure. If they want to use C in the privacy of their own bedroom, that's up to them. Of course, Linux in 2024 is written in C, mostly because Linux in 2023 was written in C, then 2022, etc all the way back to the 1990s. There's a lot of path dependence. Back in the 1990s C was a more reasonable choice to write your new OS in. Especially if it was a clone of Unix, C's original home and killer app.
    - airbreather 2y ago
      0Yeah, so I am a functional safety engineer, but for industrial process plant and machinery. We don't use C, traditionally it is safety controllers, specialised PLCs. Most safety PLC's boot into a hypervisor that boots an OS (Wind River Linux or something) that runs a program that might be your complied config, or runs a program that runs your configuration (eg code you wrote). So what languages does it seem likely were used for all those extra layers between your code and the CPU? And I am talking the sort of controllers that supervise LNG plants, large buildings where they might have more than one elevator in any shaft, prevent overpressuring pipelines and creating environmental disasters and so on. I would be more comfortable personally if I could write a c program and compile it knowing that the compiled code will run on the bare metal, at least then there are not a couple of closed source proprietary layers of abstraction between me and the processor. Note : in case you wonder what the difference between a regular PLC and a safety PLC is, a safety PLC has a fuckload more diagnostics. For a safety system PLC, faults aren't the problem, it is dangerous undetected faults. A detected dangerous fault will trip to a shutdown immediately and is an availability issue, not a safety issue. But, guess what language the firmware that does these diagnostics is written in? I don't know, but I doubt strongly it is one of the 5 PLC languages specified in IEC 61131, so that leaves it likely to be C.
  - pjmlp 2y ago
    Historical reasons, my Windows, Android, macOS, iOS devices have plenty of OS code written in C++. Even those criticial OSes that refuse to move beyond C, most likely are using C compilers written in C++.
- lelanthran 2y ago
  > No one in their right mind would write mission-critical software in C. Read my previous response to you[1]: you clearly haven't worked on systems that would kill people if things went wrong. [1] https://news.ycombinator.com/item?id=40488277 https://news.ycombinator.com/item?id=40488277
  - lisper 2y ago
    > you clearly haven't worked on systems that would kill people if things went wrong True, but I have worked on a system that would have cost hundreds of millions of dollars if things went wrong. And they did go wrong, though we managed to save the asset. So I do have some relevant experience here. Yes, if you put enough effort into it and deploy into a non-adversarial environment, you can get the odds of success pretty close to 100%. But then you also get the Therac-25 every now and then. But mainly you get an endless stream of buffer overflows that lets hackers steal people's bank accounts. That's not life-and-death, but it's a significant societal cost nonetheless.
user2342 2y ago
> My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is formally verified to preserve the intended semantics. Thats my understanding too. Code is written in high level systems generating C as output. C becomes rather an implementation detail in a hopefully, more or less completely verified tool chain.

by nequo 2y ago

lisper 2y ago

That is a noble goal, but I don't see how it can possibly achieve the intended result as long as the C standard is a fundamentally borken as it is. I tried to download CompCert so I could try it out, but they only have a source distribution and to build it you need Coq and OCaml and a few other things because of course CompCert is not written in C. No one in their right mind would write mission-critical software in C.

seabird 2y ago
If your original source is provably transpilable to C with no UB, and your compiler provably compiles that C without any bungling, then you've made it. The standard is bad and I want to see the end of C before I'm dead, but this isn't a stretch, and C is just a detail in the process.
LeFantome 2y ago
I am mostly in the other side of this argument. C is an insane language in my view ( in a modern context ). That said, what “mission critical software” are you using that is not running on an OS written in C?
- eru 2y ago
  > > No one in their right mind would write mission-critical software in C. > That said, what “mission critical software” are you using that is not running on an OS written in C? I'm not sure that's relevant? If you have a piece of mission critical software, almost all the time you run it on an existing OS like Windows or Linux. You don't _write_ a new OS just for your one piece of software. Of course, that OS had to be written at some point in the past (and is still being worked on). Presumably that writing was (and is) being done by people not 'in their right mind'. But that shouldn't concern you. The problem with C is not that you can't write secure-ish software at all; the problem is that this is insanely difficult, and that the trade-offs aren't worth it. Especially for new software. For software that I get from some third-party, like the OS, I only care about its quality (and price); I don't care about the trade-offs and pains the authors had to endure. If they want to use C in the privacy of their own bedroom, that's up to them. Of course, Linux in 2024 is written in C, mostly because Linux in 2023 was written in C, then 2022, etc all the way back to the 1990s. There's a lot of path dependence. Back in the 1990s C was a more reasonable choice to write your new OS in. Especially if it was a clone of Unix, C's original home and killer app.
  - airbreather 2y ago
    0Yeah, so I am a functional safety engineer, but for industrial process plant and machinery. We don't use C, traditionally it is safety controllers, specialised PLCs. Most safety PLC's boot into a hypervisor that boots an OS (Wind River Linux or something) that runs a program that might be your complied config, or runs a program that runs your configuration (eg code you wrote). So what languages does it seem likely were used for all those extra layers between your code and the CPU? And I am talking the sort of controllers that supervise LNG plants, large buildings where they might have more than one elevator in any shaft, prevent overpressuring pipelines and creating environmental disasters and so on. I would be more comfortable personally if I could write a c program and compile it knowing that the compiled code will run on the bare metal, at least then there are not a couple of closed source proprietary layers of abstraction between me and the processor. Note : in case you wonder what the difference between a regular PLC and a safety PLC is, a safety PLC has a fuckload more diagnostics. For a safety system PLC, faults aren't the problem, it is dangerous undetected faults. A detected dangerous fault will trip to a shutdown immediately and is an availability issue, not a safety issue. But, guess what language the firmware that does these diagnostics is written in? I don't know, but I doubt strongly it is one of the 5 PLC languages specified in IEC 61131, so that leaves it likely to be C.
- pjmlp 2y ago
  Historical reasons, my Windows, Android, macOS, iOS devices have plenty of OS code written in C++. Even those criticial OSes that refuse to move beyond C, most likely are using C compilers written in C++.
lelanthran 2y ago
> No one in their right mind would write mission-critical software in C. Read my previous response to you[1]: you clearly haven't worked on systems that would kill people if things went wrong. [1] https://news.ycombinator.com/item?id=40488277 https://news.ycombinator.com/item?id=40488277
- lisper 2y ago
  > you clearly haven't worked on systems that would kill people if things went wrong True, but I have worked on a system that would have cost hundreds of millions of dollars if things went wrong. And they did go wrong, though we managed to save the asset. So I do have some relevant experience here. Yes, if you put enough effort into it and deploy into a non-adversarial environment, you can get the odds of success pretty close to 100%. But then you also get the Therac-25 every now and then. But mainly you get an endless stream of buffer overflows that lets hackers steal people's bank accounts. That's not life-and-death, but it's a significant societal cost nonetheless.

user2342 2y ago

> My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is formally verified to preserve the intended semantics. Thats my understanding too. Code is written in high level systems generating C as output. C becomes rather an implementation detail in a hopefully, more or less completely verified tool chain.