9 votes
Accepted

Why is it impossible to prove software to be correct?

Whatever you heard is false. Proving programs correct is not only possible, it is also done in practice on large scale. There is an entire branch of computer science, namely formal methods which ...
Andrej Bauer's user avatar
  • 28.8k
4 votes

What's the difference between an invariant and an "inductive" invariant?

Just to expand on Jukka's excellent answer, the question of finding invariants usually arises when trying to establish safety properties. A safety property $S$ is a property that we wish for the ...
Motorhead's user avatar
  • 181
1 vote

Why is it impossible to prove software to be correct?

I'm wondering if you've misheard or heard a distorted version of the Donald Knuth Quote: Beware of bugs in the above code; I have only proved it correct, not tried it.' There is definitely some sort ...
Joey Eremondi's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible