Even for domains that are stable and knowable, I have to wonder what businesses can afford that kind of up-front investment before the first feature ships.
Ultimately, I think we have to make a trade-off between simplicity and easiness. The approach I outlined would be incredibly expensive because the tooling for that approach isn't quite good enough yet, and stakeholders wouldn't even understand it. They wouldn't realize that you were building a pitch for your product not as a PowerPoint deck, but as executable code!
A lot of our complexity today is from constructing software itself over layer upon layer of previous complex software (CSS, I'm looking at you), not due to the intrinsic "business cases" our software is meant to solve. Some of that complexity cannot be avoided, and some of it could be but at significant cost. To use an analogy, it's also cheaper to build a traffic light-controlled intersection, but overpasses are simpler.
Coincidentally, almost all of the tools I've seen that try to make simplicity cheaper come either from the Scheme/Racket/Lisp world that Hickey himself hails from or from Alan Kay and his sphere of influence. (The two groups have quite a bit of overlap, both in terms of ideas and even people.)
I know about Smalltalk (Squeak) so I guess that is the playground for Kay’s. Would just playing with Clojure do the same for the Hickey’s?
But even there, I suspect adaptation has to happen. Python's had how many versions over the years? Indeed, I could argue that it's one of the world's most successful languages precisely because it keeps responding to user need. Or look at tax software, which is going to change at least every year, and more often in emergencies.
So I suspect at best these other domains have a slower iteration clock. Which might be slow enough for the sort of formal modelling that is described. But then I think there's an open question: do other methods also work just as well with slow iteration clocks?
Coming up with the right abstractions and the right domain model is difficult (especially if you just sit down and try to come up with stuff, you're likely to get it wrong the first time around). Knowing about some of those things could help you come up with better abstractions, but it's neither necessary nor sufficient to ensure that you will.
Take dependent types for example. They allow you to express more program invariants or correctness properties in your types. But actually using them requires you to write proofs (at least, if you're using them to their full potential). And I do think that in general System F like type systems hit a nice sweet spot and are generally good enough for the stuff that you might actually want to handle on the type system level.
I've also run into similar "proof-like" situations with much simpler type systems like those of Haskell and Rust, where I was structuring my types to "make illegal states unrepresentable", but in the process ended up complicating my program due to having to match the structure of my program to the expected structure of the types. Sometimes it is nice to _not_ to have the type system enforce some of your invariants. (Such things are also doable with dependent types of course, but this is just an example of some of the tradeoffs involved).
You can also still have a shitty domain model even if you use all of those fancy tools. They just allow you to be very formal/precise about the domain model (and do perhaps encourage some more uniformity by making it more annoying to express ugly or complicated things).
So instead we've had to make a system which makes it less painful when bugs occur.
For us that means making it trivial to run older major and minor versions our software, and an automated update mechanism which delivers new builds to customers on-premise in less than an hour, updating the DB schema as well.
(Also, as one of my past companies enshrined as an engineering axiom: "write software to be debugged". Most programmers write waaay too few logs. You know the print statements you add to your code when it's buggy, to track down what's going wrong? Well, do that all the time, and if there are too many then fix that problem with adequate tooling. If it's running on your customers' computers - whether servers or PCs or phones - then store them locally for N days / N logs and allow them to be submitted when a bug occurs. Stack traces - even good ones - are not nearly enough.)
Once you get traction, you can start to afford to have the crazy vision. IMO, at that point it's easily worth the risk. A decent research team will probably discover something, and potentially extremely valuable knowledge.
If you were James Clerk Maxwell before he published his equations, how much would they be worth to you, especially if you had paying customers?
I submit that if we did that, we would have excellent, elegant, simple software, but following the process would be incredibly hard. So hard, in fact, that it couldn't possibly be distilled into a conference talk.