Imagine if someone released a programming language or system that made it possible and tractable to both specify, implement, and prove the correctness of, say,

Imagine if someone released a programming language or system that made it possible and tractable to both specify, implement, and prove the correctness of, say, ten different classes of things that most medium-to-large-scale programs have to deal with. Also imagine that this system had no complexity beyond the intrinsic kind. A lot of people would perhaps be initially impressed. But then they would grow to dislike the fact that the system encourages things like proofs of correctness.[1] They would dislike the fact, or the idea, that they would have to adopt to project conventions and processes that involved that kind of work in order to get their changes merged. That’s friction. And you have to deal with the intrinsic complexity more or less up-front. Then some time passes and an alternative system comes out. But this system is easier to use. It’s easier to use because it helps you 90% of the way to write and implement those same ten different things. So maybe there are no specifications, and there are certainly no proofs, and certainly no guarantess that X will always be the case or that Y will never be the case. This lack of guarantees gets lauded as “pragmatic”. In order to try to make up for the missing 10%, fuzzing libraries are written, CI pipelines are set up, everyone is encouraged to write more tests, and more process is added to code reviews. In part because “You are supposed to always do Z, anyway”. A downside is that you went from having firm guarantees (even with asterisks since they would point you to things like trusted kernels) to having no guarantees. The only guarantee that you have is right after you have run your somewhat lean six minute test suite just before committing: you know that your changes are good modulo those tests since you just ran them. Then you submit a PR and the remote CI reruns the tests. In the end, with all those code reviews and unit tests and whatnot, you look around and see only blobs of imperative code that could in principle do anything. So you add more sandboxes and security layers. Because, the low-level programmer interjects, “it’s all imperative code under the hood [anyway]”. [1] Only “encourages” since you can e.g. write stringly-typed programs even in Idris.