>However, at the end of the day, there is an input and output and compute and memory needed to run the thing and if we look at that we realize, we never actually left the bounded physical realm and we can still engineer software systems against real world constraints. We can judge its efficiency and breaking points.

This is a common sense view of computation that's unfortunately wrong.

The simplest counter example is the busy beaver program: with as little as 12 states we have saturated the computational capabilities of the universe, but it looks completely safe and sane for the first few states you would be testing against.

You may call it pathological, and you'd be right, but the point is that you never know under which rug a function that takes more computation than the universe can supply is hiding.

By comparison power electronics engineers don't have to formally prove that they didn't accidentally include a nuclear power plant in their e-scooter design.