4 ms·
What other options are there? It's the only systems level language with a formally verified compiler afaik. rust is a no go because you can't trust the compil
by yeenieee 4y ago
What other options are there?
It's the only systems level language with a formally verified compiler afaik.
rust is a no go because you can't trust the compiler's output (remember, we can't trust people to write correct code, so we obviously can't trust the compiler writers either).
- lapinot 4y agoBoth formally proven compilers and black-box SMT-based translation verification are a thing. Rust is not there yet but both exist for C.
- antientropic 4y agoThe vast majority of C programmers do not use a formally verified C compiler, and most of them wouldn't care about that anyway. From a security perspective, demanding a formally verified C compiler is rearranging the deck chairs on the Titanic. Switching to a safer language like Rust will do much more to improve security, even if the compiler is not verified.
- kaba0 4y agoThe biggest formally verified program is tiny compared to your regular software suit. That method simply doesn’t scale. Also, it “trusts the hardware” which itself can be (surprisingly) buggy. So there is no 100% safe solution, should we not even try to better our softwares then? Trusting trust is an interesting paper, but it was never meant as a gotcha, it was meant as a “don’t forget to look at the whole picture from time to time”.