aggree with most of what you said.

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.