One way in which “if it compiles, it works” can be false is that sometimes “works” is ill-defined. For instance, suppose you’re working on audio compression software. “It works” means that (1) the output is much smaller than the input, and (2) when you play it back, to most listeners it sounds just like the input did. #1 could be formalized in a way a compiler could enforce (though in some cases what you need is that the output is small for realistic inputs which isn’t so straightforward), but #2 is about what happens in humans’ ears and brains and is absolutely not the sort of thing a compiler could check.
Other examples: You’re developing a computer game; “works” means that people enjoy playing it. You’re designing a word processor; “works” means that it’s not too laborious or confusing for users to write documents that look the way they want and continue to look the way they want as they edit them. You’re writing a program that plays go; “works” means that it can beat top human players, or that its analysis is useful for top human players looking over their games. You’re writing a trading algorithm; “works” means that when you set it loose on real markets it gains rather than loses money.
What all these examples have in common is that “works” involves something about what happens when the program interacts with human beings, and human beings are complicated. (There are other complicated things besides human beings, and there are probably some good examples that don’t involve humans, but humans are really complicated, and there are a lot of us, and programs tend to be written for humans to use, and we interact with other humans … so human interaction of some sort is probably the most important source of hairiness that compilers couldn’t enforce handling correctly even in our dreams.)
I also agree with everything you said and want to add to Yair’s point that there usually is an identifiable part of the problem that involves often complex models and data structures and their modification and interaction with them via a set of primitives (an API). It would be cool if we could improve that part. It would also be cool if we could improve on the derivation and checking of the real-world-interactive part. But that requires different methods.
One way in which “if it compiles, it works” can be false is that sometimes “works” is ill-defined. For instance, suppose you’re working on audio compression software. “It works” means that (1) the output is much smaller than the input, and (2) when you play it back, to most listeners it sounds just like the input did. #1 could be formalized in a way a compiler could enforce (though in some cases what you need is that the output is small for realistic inputs which isn’t so straightforward), but #2 is about what happens in humans’ ears and brains and is absolutely not the sort of thing a compiler could check.
Other examples: You’re developing a computer game; “works” means that people enjoy playing it. You’re designing a word processor; “works” means that it’s not too laborious or confusing for users to write documents that look the way they want and continue to look the way they want as they edit them. You’re writing a program that plays go; “works” means that it can beat top human players, or that its analysis is useful for top human players looking over their games. You’re writing a trading algorithm; “works” means that when you set it loose on real markets it gains rather than loses money.
What all these examples have in common is that “works” involves something about what happens when the program interacts with human beings, and human beings are complicated. (There are other complicated things besides human beings, and there are probably some good examples that don’t involve humans, but humans are really complicated, and there are a lot of us, and programs tend to be written for humans to use, and we interact with other humans … so human interaction of some sort is probably the most important source of hairiness that compilers couldn’t enforce handling correctly even in our dreams.)
I agree with everything you just said, but in all of these cases the halting problem isn’t relevant, which is my key focus here.
Yup, that’s fair.
I also agree with everything you said and want to add to Yair’s point that there usually is an identifiable part of the problem that involves often complex models and data structures and their modification and interaction with them via a set of primitives (an API). It would be cool if we could improve that part. It would also be cool if we could improve on the derivation and checking of the real-world-interactive part. But that requires different methods.