As a matter of finesse, I think that the correctness vs productivity argument is a specious one when it comes to language design. If correctness is a business requirement then providing language support is a productivity booster for the team (when you consider the timelines of the verification process as part of the development time.) you alluded to different problem domains perhaps requiring formal proof, I just want to suggest that it may decrease the iteration time for the team as a whole.
There is also the matter that the whole "correctness vs. productivity" debate is a false opposite. There is nothing mutually contradictive with correctness and productivity, so there is no reason why you can't have both.
Correctness stems from expressing not only the algorithm but also the results you expect from running it (as types and/or test cases) so they can be verified. But if you somehow convince yourself that you haven't made any mistakes, it's always less work to just write the algorithm (and omit the expected results).
As a matter of finesse, I think that the correctness vs productivity argument is a specious one when it comes to language design. If correctness is a business requirement then providing language support is a productivity booster for the team (when you consider the timelines of the verification process as part of the development time.) you alluded to different problem domains perhaps requiring formal proof, I just want to suggest that it may decrease the iteration time for the team as a whole.