Conversation

Patrick Walton
@pcwalton
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".
22
229
Joey Eremondi @ ICFP
@EremondiJoey
I like "prove that code meets its specification." There's still an implicit "modulo your trusted base" there, but it at least captures that the proof is only as good as the spec
1
9