その辺は依存型でも使わないと無理だね
coqの例だとhead_tail : {xs:list a | ~ null xs} -> { y:a & { ys:list a | cons y ys = xs }}
みたいな型によって関数が満たすべき性質を強制することができる
ついでにコメントにもなるし、利点だけみれば静的言語の進化の方向性としては結構理想的だね
もっとも、現状ではこのスタイルで本格的な規模のコード書くとなると博士論文クラスになってしまうけど・・・