[iamevn]

I'd recommend looking into languages with either a contract system or dependent types.

https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Dependent_type

Contracts are ways to specify invariants for the runtime to verify. For example you could write a function with a contract saying that it takes a string containing all lowercase characters and returns a string containing all upper case characters. As far as the type system is concerned it just takes and returns strings but the runtime won't let a caller give you a value you don't want and won't let you return a value that doesn't match what you promised.

Dependent types essentially let you do the same but at the type level. For example you could have a function whose type says it takes a list of length N and a list of length M and returns a list of length N+M. Or maybe a type that represents a tuple containing a number N and a list of length N. Your code wouldn't type check unless the type system can prove the types. There's a lot of overlap with theorem provers in this space. Agda, Idris, and Coq are some decently popular languages in this category.

I find dependent types to be extremely powerful but sometimes the added overhead of figuring out how to encode an invariant into the type system is overwhelming.