"If the proof of program correctness requires a very large number of different proof rules, and if each proof rule has a lot of side conditions, in particular, if the validity of the local applciation of a rule to a small bit of program depends on properties which can only be established by a scan of the program as a whole, then you know that you’ve done a bad job as a language designer and you do not have to get your customers to tell you that."

— Tony Hoare