How exactly is this notion of “semantic types” formalized? Is it something like NuPRL, where the base language&#x27;s type system isn&#x27;t sufficiently precise to rule out all misbehaviors, and on top of that a more precise type system is added, whose typing rules might be defined in terms of the base language&#x27;s evaluation&#x2F;execution rules?