There is one part of your questions that I can comment on: Ronald Brown wrote:
The intuitive idea is that a program may be very complex, even undecidable, or inconsistent, but if the input is trivial, or simple, then the output may be decidable, and simple. Perhaps there are commercial examples of this, where most users give simple inputs?
Consider a Computer Algebra System (ie like Maple or Mathematica). Almost everything interesting it does in the area of Analysis is formally undecidable. This is because zero-equivalence for any interesting subset of the (constructive) reals is undecidable, and almost all CAS algorithms to do analysis (integration, solving equations, limits, simplification, etc) requires many zero-equivalence tests, amongst many undecidable problems. Nevertheless, these systems are very powerful, and frequently return interesting answers to even fairly complex user input. This is because most users give ``structured'' input, for which semi-decision procedures seem to be quite adequate. Of course, if you happen to know exactly which semi-decision procedures are being used, you can fool them and get the system to either go into an infinite loop or give a wrong answer. But that requires a huge amount of knowledge to do so. The average user would be unable to manufacture such examples. It is very important to note that the distinction is between ``structured'' input and ``generic'' input, rather than between simple and complex. In other words, what seems to matter most is the Kolmogorov Complexity (or in the specification case, the logical succinctness) of an input. [See http://www.cas.mcmaster.ca/~carette/publications/simplification.pdf for one approach to this]. There are similar examples in the automated theorem proving world, where in particular PVS and IMPS can frequently prove theorems which are not a priori known to be in a decidable subclass. Here again, a combination of semi-decision procedures driven by intelligent heuristics seems to be highly effective. Jacques