&quot;You always need more bits of axioms than of program if you want to prove theorems about your programs.&quot;<p>Fascinating. Is that a quote? I&#x27;ve never seen it stated that way. I think something about it just clicked for me.