u/lightmatter501in r/programming • Recommends
On “The empire of C++ strikes back with Safe C++ blueprint: « After two years of being beaten with the memory-safety stick, the C++ community has published a proposal to help developers write less vulnerable code. »”
There is a difference between absolute safety, which Agda, Idris, and a subset of Haskell offer, where you do constructive formal verification and the compiler is formally verified to only perform valid transformations of code, and “the normal mode of this language will never let you read off the end of an allocation or deref a null pointer”. The latter is accomplished by Java as well, with James Gosling saying that Java exists because of C and C++ pointer bugs.
It turns out that if you want to formally verify a language, it’s actually very reasonable to formally verify transformations in the compiler as valid down to some IR, then prove the properties of the IR. That’s how formally veri…