Yes, I replied to the one I meant to. The reason we use type systems is that they let us prove things about our code: simple things like “this is a string, not an int”, more complicated things like “this variable cannot be null”, and to the advanced “I have written up a proof in a theorem-proving language that this program will not deviate from the published specifications in these ways”. My point is that the thing that people really want to prove, which is obviously “does this program work and do so correctly”, is fairly impossible to do so in practice due to some of the problems I mentioned. You can only approximate at this along certain domains.

I agree. Some lower level library could be rigged to return an Authorized<UserId> when that user is in fact not authorized.

So we would have to make sure that type safety is ultimately backed by a hardware based encryption module, but that's just not where we are today.