I'd bet you could ensure that some kind of tolerance and stability checks were performed and then carry the results around. Ultimately whenever computation reli

I'd bet you could ensure that some kind of tolerance and stability checks were performed and then carry the results around. Ultimately whenever computation relies on dynamic input it's necessary to have a hard-coded "tolerance failure" check. Theoretically you could embed enough analysis in there to have theories about the actual code you're running, too, but I don't think as many analysts care about theorem proving—they're more of an algebraicist's toy.