Assumptions weaken properties

<p>In <a href="https://buttondown.com/hillelwayne/archive/some-tests-are-stronger-than-others/" target="_blank">some tests are stronger than others</a>, I defined <code>STRONG =&gt; WEAK</code> to mean "any system passing test STRONG is also guaranteed to pass WEAK". This uses the logical implication operator, defined as <code>P =&gt; Q = !P || (P &amp;&amp; Q)</code>.</p> <p>Implication may be the most overworked operator in logic. Among other things, it's also used in formal specification, where <code>Spec =&gt; Prop</code> means "any system satisfying <code>Spec</code> has property <code>Prop</code>" and <code>ASSUME =&gt; Spec</code> means "The assumption <code>ASSUME</code> must hold in order for the system to satisfy <code>Spec</code>."</p> <p>Now let's mush these all together and do some math. To start, "the system has property <code>Prop</code>" is the same as "the system passes the test that checks <code>Prop</code>", so test strength is also property strength. Now let "<code>ASSUME =&gt; Prop</code>" mean "the system passes <code>Prop</code> assuming <code>ASSUME</code> is true." In classic logic, if <code>P</code> is true, then obviously <code>!Q || P</code> is true. Further, that is equivalent (just draw the truth table!) to <code>!Q || (P &amp;&amp; Q)</code>. So for <em>any</em> propositions <code>P</code> and <code>Q</code>, <code>P =&gt; (Q =&gt; P)</code>.</p> <p>In other words, <code>Prop =&gt; (ASSUME =&gt; Prop)</code>. In other other words, "the system passes <code>Prop</code>" is a stronger property than "the system passes <code>Prop</code> whenever our assumptions hold."</p> <p>In other other other words, any assumption added makes a property weaker.</p> <p>This makes intuitive sense to me. A JSON parser that's only been verified with ASCII strings has the property "input only uses ASCII &amp;&amp; is valid json =&gt; correctly parsed". A better JSON parser that works for all Unicode will have the property "is valid json =&gt; correctly parsed", which has fewer assumptions, meaning it's guaranteed to work in a strict superset of cases. </p> <p>It also matches the intuition that "more assumptions means more likely to go wrong". We have a bug whenever <code>Prop</code> is false. The only way for <code>Spec =&gt; Prop</code> to be true and <code>Prop</code> be false is if <code>Spec</code> is false, eg our system doesn't satisfy the specification we intended to implement. On the other hand, <code>Spec =&gt; (ASSUME =&gt; Prop) &amp;&amp; !Prop</code> is true whenever <code>Spec</code> <em>and/or</em> <code>ASSUME</code> is false, meaning a correctly-implemented system could still show a bug if a runtime assumption is false. </p> <p>...Looking back the last two paragraphs have a lot of conceptual leaps. Does that all make sense to you? It all feels natural to me but that might just be my familiarity with the topic talking. </p> <p>Regardless, a couple more notes on assumptions:</p> <h2>Why we have assumptions</h2> <p>Why not just build our systems to satisfy <code>ASSUME =&gt; Prop</code> when we can "just" build it to satisfy <code>Prop</code>? At least three reasons.</p> <p><strong>First</strong>, sometimes <code>Prop</code> is simply impossible to satisfy and we need to add assumptions to make this property. We do this a lot in formal methods with <a href="https://www.hillelwayne.com/post/fairness/" target="_blank">fairness</a>. The property "<code>mergesort</code> always returns a sorted list" is unsatisfiable because we can dropkick the computer before it returns. Instead, we have to verify a weaker property like "<code>mergesort</code> always returns =&gt; it returns a sorted list" or "<code>mergesort</code> always makes progress =&gt; it will eventually return a sorted list."</p> <p>Another example is Rust. Rust <em>does not</em> guarantee the property "the program is memory safe". It guarantees the weaker property "all <code>unsafe</code> blocks are memory safe =&gt; the program is memory safe". Making the language satisfy the stronger property would rule out too many use cases of Rust. Note you also get memory safety if you don't use <code>unsafe</code>, but that still satisfies the assumption, as all <em>zero</em> blocks are safe!</p> <p><strong>Second</strong>, sometimes the strong property is satisfiable, but it's simply not worth the extra cost. Like it's possible to make our software resistant against cosmic rays, but if your code isn't running in space, why bother? Just say "No cosmic bit flips =&gt; things work". Or if your plugin works Neovim <code>0.12</code> but not 0.11, you could put in the effort to make it run on older versions, or you could tell everybody that they need to upgrade to use your plugin. "Neovim version is at least 0.12 =&gt; the plugin works".</p> <p><strong>Third</strong>, sometimes the strong property is satisfiable in the system but not easily <em>verifiable</em>. Say your algorithm makes a lot of API calls and you don't want to hit rate limits while testing. If you <a href="https://en.wikipedia.org/wiki/Mock_object" target="_blank">mock out the API</a> you're testing the weaker property "The mock is accurate to the API =&gt; the algorithm is correct".</p> <h2>Assumptions are a second level of system effect</h2> <p>I notice that almost all of the examples in the last two sections are exoprogram factors:</p> <ul> <li>The JSON parser assumptions are about user input</li> <li>Fairness assumptions are about the OS/hardware/operating environment</li> <li>Unsafe assumptions are about things the Rust compiler can't verify</li> <li>Cosmic ray assumptions depend on the physical location of the hardware</li> <li>The plugin assumptions are about the Neovim team's release schedule and social compatibility contract</li> </ul> <p>The edge case is replacing a third party call with a mock. The assumption is intraprogram because the program could just hit the API during testing. We still have the assumption because of an exoprogram constraint. Maybe this is why mocks are considered an antipattern in Agile.</p> <p>One consequence of this is that checking whether assumptions hold is a different problem from verifying that your code works given the assumptions. Like to make sure "all unsafe blocks are safe" can't use the rust compiler, you need a second tool like <a href="https://github.com/rust-lang/miri" target="_blank">Miri</a>. I wonder if checking assumptions is, in practice, generally more difficult than checking everything else.</p>