[tbct]

Surely, however from a software architecture perspective types as contracts, assuming pure functions and maximally restrictive types, is a good model for reasoning about a system. A function such as:

addIfEven: Int -> Int -> Maybe Int

even without knowledge of the implementation lets us know our caller has 'entered into a contract' where addIfEven will reduce two integers depending on some conditions. This contract then becomes two-wayed: If I modify the implementation of the function there's a good chance I'll be forced to modify the signature, thereby letting me know statically that I've broken the contract with the callsite.

I'd recommend checking out https://lexi-lambda.github.io/blog/2020/08/13/types-as-axiom... for a far better write-up than this comment on why type-driven development is like unlocking a cheat-code for development.