Can&#x27;t believe this has 52 points and no comments as such.<p>I enjoyed this video.<p>This was the first time I properly felt that proof rewrite rules are essentially our attempt to capture the squishy notions of &quot;this is what we informally do when we prove stuff&quot;.<p>It got me thinking in terms about what is permissible or allowable. So, Logical And Introduction is: You&#x27;re not allowed to use -- use, in the sense of introduce -- &amp; unless you know (that) A and you also know (that) B.<p><pre><code>   A   B
   ----- &amp;-I
   A &amp; B
</code></pre>
It got me thinking that it&#x27;d be neat to have a programming language with logic-system annotations. For instance, if in Haskell Monads are equivalent to Modal Logic then it&#x27;d be nice to be able to partition programmes by logic-system casting. Probably overkill for day-to-day programming. But it&#x27;d make for better static analysis I&#x27;m sure. Also, the notion of safe&#x2F;unsafe in some programming languages could be subsume into this machinery when you think about it, for instance instead of<p><pre><code>   unsafe fn()</code></pre>
you&#x27;d have<p><pre><code>   logical-system(null) fn()</code></pre>
if you see what I mean.