Comment by wongarsu
11 days ago
There is a formally proven compiler for a large subset of C, so I don't see why formalizing (a large subset of) rust and making a formally proven compiler shouldn't be possible
11 days ago
There is a formally proven compiler for a large subset of C, so I don't see why formalizing (a large subset of) rust and making a formally proven compiler shouldn't be possible
Also unlike C, it should be possible to formalize all of Rust, not just a subset. For two reasons: Rust evolution (not initially but today) is strongly tied with formalizing it and the language team consults with formalization experts (which are part of the Rust project themselves) all the time (and formalization or semi-formalization projects are ongoing), and also the mathematical understanding of system languages itself has advanced.
This reminds me of Hilbert’s Program .
You got my reference. But the original comment stands at -1 points now, even mock criticism of C and Rust seems to be totally unappreciated by the bigots.
It is possible to formalize all of C.
Perhaps. We don't know for sure. We also don't know for sure about Rust, but the odds here are greater.
There is a severe misunderstanding here. Beside being only a subset, CompCert definitely has UB. It just formalizes codegen for codebases not containing UB, which obviously won't be enough for Rust.
Because people want a performant optimizing compiler.
CompCert produces surprisingly fast native code.
This 2022 article [0] says it generates binaries that run about 7% slower than what GCC produces with -O1.
[0] https://www.cs.cornell.edu/courses/cs6120/2022sp/blog/compce...
That's a big gap, especially with the norm for releases being O2 if I understand correctly.
3 replies →