"Strong typing vs. strong testing"
gene.ressler at gmail.com
Thu Sep 30 22:06:53 CEST 2010
On Sep 30, 3:45 pm, RG <rNOSPA... at flownet.com> wrote:
> In article <7xr5gbxfry.... at ruckus.brouhaha.com>,
> Paul Rubin <no.em... at nospam.invalid> wrote:
> > RG <rNOSPA... at flownet.com> writes:
> > > Yes, I know I could have used lint. But that misses the point. For any
> > > static analyzer, because of the halting problem, I can construct a
> > > program that either contains an error that the analyzer will not catch,
> > > or for which the analyzer will produce a false positive.
> > Can you describe any plausible real-world programs where the effort of
> > complicated static is justified, and for which the halting problem gets
> > in the way of analysis? By "real world", I meanI wouldn't consider
> > searching for counterexamples to the Collatz conjecture to qualify as
> > sufficiently real-world and sufficiently complex for fancy static
> > analysis. And even if it did, the static analyzer could deliver a
> > partial result, like "this function either returns a counterexample to
> > the Collatz conjecture or else it doesn't return".
> > D. Turner wrote a famous paper arguing something like the above, saying
> > basically that Turing completeness of programming languages is
> > overrated:
> > http://www.jucs.org/jucs_10_7/total_functional_programming
> > The main example of a sensible program that can't be written in a
> > non-complete language is an interpreter for a Turing-complete language.
> > But presumably a high-assurance application should never contain such a
> > thing, since the interpreted programs themselves then wouldn't have
> > static assurance.
> There are only two possibilities: either you have a finite-state
> machine, or you have a Turning machine. (Well, OK, you could have a
> pushdown automaton, but there are no programming languages that model a
> PDA. Well, OK, there's Forth, but AFAIK there are no static type
> checkers for Forth. Besides, who uses Forth? ;-)
> If you have a finite state machine everything is trivial. If you have a
> Turing machine everything is generally impossible. This is an
> oversimplification but not far from the fundamental underlying truth.
> My favorite practical example is the square root function. The standard
> C library defines a square root function on floats (actually on
> doubles), which is to say, over a finite-state model with 2^64 states.
> The model is not well defined over half of that range (negative
> numbers), which the static type checker cannot catch because there is no
> such thing as an unsigned double.
> But the fun doesn't stop there. Doubles >= 0.0 are not the only thing
> one might reasonably want to take a square root of, and indeed C++
> overloads sqrt to work on complex and valarray types in addition to
> floats of various lengths (though you still have to manually keep track
> of whether or not the argument to sqrt might be a negative real). But
> what if I want an exact integer square root? Or a square root of a data
> type that represents irrational numbers not as floating point
> approximations but as exact symbolic representations? I haven't worked
> out the details, but I'd be surprised if none of these variations turned
> out to be Turing complete.
> The Turner paper is right on point: there's a fundamental distinction
> between the (known) finite and the (potentially) infinite. In my
> experience most of the cool interesting stuff has been found in the
> latter domain, and trying to shoehorn the latter into the former is more
> trouble then it's worth.
The FA or TM dichotomy is more painful to contemplate than you say.
Making appropriate simplifications for input, any modern computer is a
FA with 2^(a few trillion) states. Consequently, the gestalt of
computer science seems to be to take it on faith that at some very
large number of states, the FA behavior makes a transition to TM
behavior for all possible practical purposes (and I mean all). So
what is it--really--that's trivial to analyze? And what is
impossible? I'm sorry this is drifting OT and will stop here.
More information about the Python-list