This is one of my main criticisms of many FM projects, including ones I've worked on. To be fair, our papers usually are very clear about what assumptions are being made and what specifications are being used, but the marketing and informal discussion usually overstates the case.
Quote Tweet
I'm resolving to stop using the phrase "prove code correct". You prove specific theorems about codebases relative to some domain model. "X is proven correct because it was formalized in Coq" is as inaccurate as saying "X is proven secure because it was written in Rust".
2
13
