Can'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 "this is what we informally do when we prove stuff".<p>It got me thinking in terms about what is permissible or allowable. So, Logical And Introduction is: You're not allowed to use -- use, in the sense of introduce -- & unless you know (that) A and you also know (that) B.<p><pre><code> A B
----- &-I
A & B
</code></pre>
It got me thinking that it'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'd be nice to be able to partition programmes by logic-system casting. Probably overkill for day-to-day programming. But it'd make for better static analysis I'm sure. Also, the notion of safe/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'd have<p><pre><code> logical-system(null) fn()</code></pre>
if you see what I mean.
Yes, you can do that. You can write x ∈ 𝕀 ∧ x ≥ 0 to express "unsigned x". This allows some useful operations on type propositions. But it doesn't scale well to structs and objects.