I believe he means compile-time checks. Th formal term for this is dependent types. Some languages offer it. Haskell is working on making it ergonomic. It's alr

I believe he means compile-time checks. Th formal term for this is dependent types. Some languages offer it. Haskell is working on making it ergonomic. It's already quite ergonomic in Idris.