2 ms·

that usually gets classified under contracts rather than types. eiffel is probably the best known example of a contract based language, but also check out typed

• galaxyLogic 4y ago
  That is good vocabulary. Clearly there is a difference between static type-checking and assertions. But "types" is not the same as "type-checking". Type-checking can happen at runtime, or at compile-time. Or both. My point was more that static type-checking can be seen equivalent to assertions, except it checks those assertions at compile time and typically lacks some expressive power compared to assertions, in most practical programming languages today. Static type-checking is more a feature of the compiler than of the language. Consider type-inference: You can have a language where types are not explicitly declared most of the time. Yet they can be checked at compile-time, assuming you have a compiler that is able to perform that amazing feat.