"What killed Smalltalk? it was just too easy to make a mess" (Ward Cunningham) The power of your tools is an orthogonal issue. It isn't related to the discipl

"What killed Smalltalk? it was just too easy to make a mess" (Ward Cunningham) The power of your tools is an orthogonal issue. It isn't related to the discipline and cleanliness issue: for example, dynamic typing allows you to make design miracles, as well as stinking piles of obscure-broken-beyond-repair code. Actually, a lot of powerful tools have this double-edged sword quality: dynamic typing. C++ templates. shared_ptr/garbage collection. inheritancy. lambdas/closures. "eval". monkey patching. tests (!). Sure, tools like Coq or even Rust's static type system will provide, at compile time, extra guarantees that your code will work as intended. However, they won't provide guarantees that your program will be easy to maintain/modify. Actually, if misused, they could have the opposite effect (i.e as soon as you try modifying the smallest bit of code, compilation/checking fails with unhelpful error messages). Don't get me wrong: good tools are important, and nobody's going to make me write a webserver in assembly language, or a NES emulator in PHP! However, in my experience, their impact on code maintainability is negligible in front the impact of the developper herself. Ultimately, it all hinges on who's writing the code.