"Strong typing vs. strong testing"

[Paul Rubin]

RG <rNOSPAMon at flownet.com> writes:
> 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.

The point is that the halting problem for general Turing machines is
undecidable, but there is a subset of the Turing machines, in which the
halting problem is decidable.  And it turns out that the decidable
subset is substantial enough to write almost every program anyone
usually wants to write in practice.

> Well, OK, there's Forth, but AFAIK there are no static type 
> checkers for Forth. 

   http://home.vrweb.de/stephan.becher/forth/

but anyway, Forth is Turing-complete.

> 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.

I'm sorry, but I don't think you understand the actual situation enough
to be making pronouncements like that.  The stuff about finite-state
machines isn't even slightly relevant. 

> 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 point of the Turner paper is that you can design a language with
separate types for finite data (like arrays) and "infinite" data (like
an endless stream of requests going into a server).  Such a language can
restrict you to writing provably halting programs on the finite data,
and provably non-halting programs on the infinite data.  That is, the
language doesn't let you write infinite loops on finite data or break
out of infinite loops on infinite data (you can only shut down your
server by "unplugging the computer", e.g. by killing the process
externally).

The claim is that these two classes of programs are enough for most
purposes.  The third possible class, the programs like the Collatz
searcher where you can't tell by static analysis whether the program
halts, just isn't that important.  The paper argues that by giving up
the ability to express those undecidable programs, a language can gain
other advantages that make up for the loss of Turing-completeness most
of the time.

I don't think anyone has suggested languages like that are a great idea
for everyday programming, but obviously there can be metholodogies that
use such approaches for special purposes.