Biological systems are logical too. The genome is the program that is hardwired into them. They also run on mathematics involved in chemical reactions. Even the simplest organism like the single-celled amoeba has more complicated and highly optimized algorithms programmed into its genome for survival than the most complex system (like the LHC) ever built by humans. An amoeba behaves the way it behaves because the laws of physics imbued in the mathematics of its chemical reactions caused it to overwrite its own gene code in such a way so as to optimize the mathematical probability of its own survival. Mathematics is merely an abstraction of our mind to understand the reality of our world. The programs that we create solve problems in our world, but are constrained by the same kind of variables that constrain biological systems, but both biological and software systems could be interpreted in terms of mathematics.

No real world biological or physical system is 'simple'. Every program starts simple, but even that is up to interpretation. A one liner program in any language is extremely complicated once you factor in the OS, the compiler and the interpreter that will actually run this program. Once the program intakes more complicated functionalities, and also multiple programmers, it becomes anything but simple. Simplicity is good to organize our thoughts and design systems, but it a whole different matter to expect that the designed system will also stay simple. Hence just like any other system in nature, software also has to evolve, and there shouldn't be anything wrong with that. A mathematical proof is not a panacea for the problems in software development. The purpose of software changes, its constraints change, and proofs will have to be rewritten everytime. You don't expect the underlying laws of mathematics to change, that is why once proved, a theorem stays proved. But in software it is expected that the system's underlying purpose will change with time. So proving the current state is what we can do, which is not of much consequence as time goes by.