In recent years there has been a lot of improvement in refinement types which is, from what I understood, what you are describing. See for example Liquid Haskel

In recent years there has been a lot of improvement in refinement types which is, from what I understood, what you are describing. See for example Liquid Haskell that uses Z3 solver for static verification. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ I'd say that when dependent + refinement types get more mature and get pass the basic prototype idea in research languages/environments, these ideas could easily transfer to mainstream static typed languages and be a new module of future compilers.