On Propositions as Types [video]

Can't believe this has 52 points and no comments as such.

I enjoyed this video.

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".

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.

   A   B
   ----- &-I
   A & B

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

   unsafe fn()

you'd have

   logical-system(null) fn()

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.