The benefits of such an approach would be substantial. However, nobody has gotten the costs down below "eye watering", or similar other metaphors. It's not that

The benefits of such an approach would be substantial. However, nobody has gotten the costs down below "eye watering", or similar other metaphors. It's not that it can't be done, it's that it is not yet known if it can be done in a way that comes out positive on the cost/benefits engineering analysis. I am open to the possibility that it can, but at the same time, I'd say if I draw the trendline of progress in this area out, it's not really all that encouraging. If you want to see why it has remained only academic, spend some time with Idris and take notes on how many problems you encounter are fundamental to the paradigm versus problems that can be solved with a larger involvement of effort. You'll want to pick a task that fits into its library ecosystem already, and not something like "hey, I'll write a fully generic HTTP server that can be proved correct" on your first try. I seriously suggest this, it's very educational. But part of that education will probably be to tone down your expectations of this being a miracle cure any time soon. I don't say this to celebrate the situation; it's a bummer. But if the situation is ever going to be solved, it's going to be solved by people viewing it clearly. (One of the major problems I see is that when you get to this level of specification, you end up with everything being too rigid. It is true that a lot of programming problems arise from things being made too sloppy and permitting a lot of states and actions that shouldn't exist. But some of that slop is also what makes our real-world systems compose together at all, without the original creator having to anticipate every possible usage. The "richer" the specifications get, the more rigid they get, and the more the creator of the code has to anticipate every possible future usage, which is not a reasonable ask. While I'd like to have the option to lock down many things more tightly, especially certain high-priority things like crypto or user permissions, it is far from obvious to me that the optimum ideal across the entire programming world is to maximize the specification level to this degree. And those high-priority use cases tend to jump to mind, but we also tend to overestimate their size in the real world. If we are going to see this style of programming succeed, we need to figure out how to balance the rigidity of tight specification with the ability to still flexibly use code in unanticipated manners later, in a context where the original specifications may not be quite right, and I think it's pretty unclear how to do that. Tightening down much past Haskell seems pretty challenging, and even Haskell is a bridge or three too far for a lot of people.)