Conversation

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".

229

Brendan Zabarauskas

@brendanzab

Apr 23, 2021

Subtweeting here, but this is similar to why it annoys me a little when I hear 'programs in X have no bugs'. Like, yeah you have type system that verifies you won't have unhandled exceptions and type errors, but the type system in question isn't rich enough to avoid logic bugs!

Replying to

and

And even if you did have that there's no guarantee that your types/specifications are actually what you want - you're just localising the place where bugs can occur.

12:18 AM · Apr 23, 2021Twitter Web App

Replying to

and

Programs written in #!/bin/cat have no bugs, but in that programming language you may only write quines and nothing else. ;)