@whitequark yeah, that's definitely a fair abstraction as we tend to live there all the time and i would probably hold that position in some context too.
it's very tied to value use in a specific context though, and also breaks down at the other end - the very very high level space - where there are many types that never manifest and are never really subject to checks in the common ways, but humans talk about entirely independently of any program or implementation