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.

Assuming that spec can genuinely embody everything you care about, about the code. Is this currently possible for performance metrics, anywhere?

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.

Yeah, absolutely. I said "if" rather carefully, ha.

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 :)

He never posited that code couldn't be proven correct by formal methods, only that he doesn't assume the type system compiling it makes it correct.

Perhaps mathematical proof + comprehensive test suite (including property/fuzz testing) + (time used without bugs showing up * number of people using it)

This does not prevent you from proving the program correct by hand. Regrettably that is rarely done, but could in principle be done regardless of the type system of the language. Of course that would require you to write a specification of the of the features you want to implement, which might be messy depending on your problem domain.

I tried that once at a small piece of code, however the problem was that there was no way to verify the code implemented what the proof said about it.

I'm not sure what this has to do with me. Again, I never said you can't prove programs correct. I simply stated how I work: I don't run my code nearly as often as I would when working in C.