Comment by hulitu

> It is not practical to prove correctness for the vast majority of programs,

That is the excuse i hear a lot from software developers, when everything they do is to test the expected behaviour of a program, without any edge case.

And this is also the reason why iMessage and WhatsUp are full of one click exploits.