形式検証と契約プログラミングって、型のデザインが過度に複雑にならずに安全性を高められるって点でも、むしろ初学者に優しくなるかも＞＜

完全に型のみに頼れば、たとえば引数が0では無い整数である必要がある時には、『0では無い整数型』が必要になるし、結局どこかでその型への明示的な(あるいは暗黙の)型変換が必要になる＞＜

でも、怠慢なプログラマは、ゼロになっていないかのチェックを事前に行わずに、型変換時のエラーに任せるコードを書いちゃって、実行時にエラーが出るか、または出ないけどロジック的には誤りになるコードを記述してしまい、わざわざ『0では無い整数型』を導入したメリットがほとんど無くなっちゃう＞＜

形式検証であれば、実際のロジック部分(？)で「ゼロになる可能性があるのでその対策が必要なこと」をエラーまたはアドバイスにすることができ、
オプショナルで無視するつもりなら無視しておいて実行時のエラーに任せるという選択も出来て、同じ無視する場合でも型で記述する方式と比べると無駄な型変換コードが節約できる＞＜
そういう面でも初学者に易しいかも＞＜