I've never seen a type system expressive enough to cover all the things that contracts can do, e.g does a type system exist which can assert the existence and size of a particular file on disk?