Haskell is not quite sufficient to connect mathematical proof to your code. Coq/Agda/Idris are much closer to this idea though and, if you can create a spec in one of those systems then a proof really is sufficient.
You can express "this code performs at most n primitive steps from this list". Theoretically it should be possible to express any performance requirement in that form, but I doubt it's practical to do for e.g. numeric computation. (It's usable for "no page render require more than 4 db roundtrips" or similar though).
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.
That you did. I certainly didn't mean it as a takedown! I just saw it a subtlety worth stressing, and about which I was eager to learn more if there was more to learn :)
