3 ms·
What do you call seL4, the Compcert C compiler and the tools for writing provably correct C at frama-c.org?
by ryao 4y ago
What do you call seL4, the Compcert C compiler and the tools for writing provably correct C at frama-c.org?
- quotemstr 4y agoThat's called a Chinese Room. :-) A human cannot write correct C. The theorem-prover-human system can. Unfortunately, the C apologists I observe around me are as opposed to formal methods as they are non-C languages. It's some kind of bizarre cowboy thing.
- Quekid5 4y agoI'd call that a straw man. Very little code is written that way, so it doesn't apply in practice, like... at all. Also: unless you have very specific requirements there are probably easier languages+tools to write proven-correct programs in.