For me it seems more like modern software has built away from using formal mathematical models in the first place, not the necessarily the problem people want to solve have to have such a fuzzy definition of domain, but that the primitives of operating systems and software development have gone in the other direction.

Think about the filesystem, the big issue with formalizing a program spec that operates on a file system is simply the fact it is essentially a shared object amongst all the programs running on the system. Add to that the fact that (though this changes with modern containerization systems, namespaces, pledge what ever) a program may at any point gain access to root permissions if it makes the system call to do so providing the correct credentials it becomes very difficult formally be able to remove any possible states from the system.

All this could be different but we would radically need to redesign are systems and the way we think about the problems.