That reminds me of a wonderful, surely apocryphal story I was told by an old boss who went to grad school at Cornell in the 1970s.

The story goes that there was some talk about the Cornell computer science department doing nothing but ivory tower mathematics that was useless to people who actually, you know, used computers in their research — such as the physicists programming data collection controllers for the particle accelerator. This concerned the head of the CS department as the harsh talk was creating a little bit of mutual resentment, not to mention an image problem for his department. He resolved to help bridge the theory-practice divide and show the non-CS computer users on campus that his theoreticians were doing worthwhile work.

So one day a CS professor schedules an intro talk on formal methods, nothing but basic mathematical maturity required, and the department chair seizes his chance! He invites a bunch of the particle accelerator folks to the talk, telling them formal methods will help them write more reliable code so they don't waste their time re-running experiments because of data collection errors. The physicist roll their eyes and shake their heads, but when the hour rolls around, some of them are present at the back of the room.

The professor gives a pretty standard formal methods talk, introducing a hypothetical (of course) programming language, showing how mathematical propositions about a program can be formulated and proved, defining a simple mathematical problem involving coloring a graph, and demonstrating a proof of correctness for a solution in the hypothetical programming language.

The physicists are impressed but a little wary. After all, their problems are mostly with performance rather than the kind of correctness addressed in the lecture. One of them raises his hand. "Is it possible, using these methods, to bound the number of times each subroutine is called?"

The CS professor, who has been instructed to engage the physicists and be very accommodating and diplomatic, is delighted by the question. "Yes! We can formulate an answer in terms of the input and prove it by recursion." He turns to the blackboard and formulates the statement and a proof. "There we have it. And I must congratulate you on such an interesting theoretical question."

"I'm actually getting at something very practical," the physicist replies. "Namely, performance. This program isn't worth much if it takes too long to solve the problem."

The CS professor narrows his brow and says, "Hmmm, I see. Yes, that can be a concern sometimes. Well, I hope these ideas have put all your fears to rest on that topic!"

"I'm afraid it's not so obvious to me," the physicist says.

"Well, we've proved the program terminates, and that when it terminates, it produces a correct solution. We can prove various other properties such as which solution will be produced if there are multiple correct solutions."

"There are other properties of the program that are of interesting as well. Can you prove whether runs within certain memory bounds?"

The CS professor starts to look profoundly bored. "Yes, these methods could be used for that. Space and time bounds can be very interesting."

"Wonderful, wonderful! So if I need to be sure that this code runs in, say, 50 milliseconds...."

"Runs? In 50 milliseconds?"

"Yes, supposing I want to run it hundreds of times per second, I..."

"Hold on a second, I don't think you've got the point after all. You never have to run the program. That is why" (the CS professor gestures at the chalkboard) "we have done all of this work! You never have to run it, because you already know it produces the correct answer!"