I think liquid types, ala Liquid Haskell are a preferable middle ground in this scenario. The SMT is built into the type checker and the refinements are limited to a linearly decidable proof fragment. Dominic Orchard has done some work generalizing the capabilities of these types of refinement by showing that the refinement fragment need to just be a semi-ring structure and the SMT can still resolve. This would cover a large portion of contracts and not impart the development process in large part.