> Software doesn't exist in a platonic state like formal mathematics

Doesn't it? Like all these things you can model in the end, your state space, and thus necessary proofs and even just the spec itself would explode in size.

But that's how every single model works.