Yes. Does yours not? Tools like Agda, Spark, Idris, and Coq move the tradeoff around towards "probably correct", and I welcome seeing some of their features be

Yes. Does yours not? Tools like Agda, Spark, Idris, and Coq move the tradeoff around towards "probably correct", and I welcome seeing some of their features become gradually available. Getting things right the first time is useful. But these features can also make it hard to get anything done quickly. Good developer experience means finding a balance between the quick and dirty, and the provably correct.