"By investigating the logical properties of your programming language and finding out how difficult it would be to prove correctness if you wanted to, you would get an objective measurement of how easy the language was to use correctly."

— Tony Hoare

"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