Exactly. My experience building a system that generates Dafny and Liquid Haskell is that you can get much further than with a language that is limited to dynami

Exactly. My experience building a system that generates Dafny and Liquid Haskell is that you can get much further than with a language that is limited to dynamic or simple static types.