back
1 comments
Since it's on HN, I'll note that the main signifigance of CakeML is that popular provers extract to Standard ML. It's the common denominator that was designed for provers. Aside from spec errors, the remaining areas with potential for errors are extraction from specs to code and compilation from code to binary. Some other work verifies extraction. Then this and other work verify the hardware. They're trying to fill in a the gaps in a way that ties them together.