🚀 go-pugleaf

gudeman@cs.arizona.edu (David Gudeman) writes:

  >Every time I see something like "I use statically typed languages for
  >security..." I grit my teeth and heroically try not to hit the
  >follow-up key (with more-or-less success).  No one has yet presented
  >anything resembling evidence that the above is a true statement. 

Since static or strong typing is a well established paradigm of software
engineering I guess you are in the position to present some 
arguments of evidence against it, arent you? Anyway, you did ...

  >My argument is that: (1) the type errors that are caught by static
  >typing are the easiest kind of errors to find by testing -- so static
  >type checking is of no real value for product security.  

To repeat, what several people already pointed out:
This depends strongly on the kind of application. I dont know what
kind of application you are dealing with. I would suspect at least
with the following ones you might get some serious troubles "trusting
in testing":

a)	Real-time applications, e.g. network-protocols. Here holds
	the Heisenberg syndrome ... you cannot observe them objectively.

b)	Sophisticated interactive systems: you cannot imagine all the
	possible action-sequences the user might performe.

c)	Complex data transformations, e.g. optimising compilers:
	there are always some exotic combinations of input
	data you missed to take into account in your test suite.

You claim, that the errors caught by static typing are trivial ones.
This is usally right. However, my experience is that most bugs of the
kind you are searching for days over days are finally of trivial nature. 
Logical errors are much more easy to recover; actually, most of 
them will be detected during the implementation phase.

The principal point here is related to the paradigm of compositionality
of software pieces. This claims it should be possible to compose 
correct pieces of software yielding a new correct piece of software 
with semantics formed from the semantics of the software pieces and the 
semantics of the composition operator. 

A trivial error in one piece under composition becomes a less trivial
error in the composed result and so on. 

One way to avoid such errors is to force some kind of compatibility 
condition for the software pieces under composition which is checkable 
by a tool. The easiest and indeed most restrictive way for this 
is monomorphic typing as known from C, MODULA-2, etc. But there are
more sophisticated models of typing already applicated 
(parameterization, subtyping) and even more sophisticated under research
(dependent types, parameter constraints, etc.), which the 
fans of dynamic typing permantly ignore.

  >And (2) the
  >complex declarations required by static typing can be sources of
  >hard-to-find errors.  (Complex declarations does not mean the
  >requirement to declare the types of variables, but of structures and
  >generic functions.)

I cannot follow you here. Several people already pointed out that
the requirement of type declarations is not connected
with the requirement of strong or static typing (see ML, Haskell). 
	
Its right that especially in a language with type unification some
raised type errors are hard to fix (ever get the message "Type 
error in RHS of equation" or how it was called in HOPE?). But this
just shows that there are also non-trivial type errors.

>--
>					David Gudeman
>gudeman@cs.arizona.edu
>noao!arizona!gudeman

--
Wolfgang Grieskamp 
wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET