[plt-scheme] Why do folks implement statically typed languages?

On Thu, May 31, 2007 at 12:05:53PM -0400, Matthias Felleisen wrote:
> 
> On May 31, 2007, at 11:46 AM, Noel Welsh wrote:
> 
> >Just came across this:
> >
> > http://www.sans-ssi.org/top_three.pdf
> >
> >It lists the top 3 errors causing security holes.  They are:
> >
> >1. Using unvalidated user input.
> >2. Buffer overflow
> >3. "Handling integers incorrectly"
> >
> >The former could be solved with a static type system.  It can also be
> >addressed with dynamic checks with the usual tradeoffs.
> 
> If you mean the 'first' I absolutely disagree. I bet that these are  
> all about 'parsing' in the sense of read-line strings or collecting  
> and consistency checking the status of GUI widgets.

The point here is. I think, not failing to code proper validation 
routines, but failing to call them.  If the type if input is 'string' 
instead of 'checked-string' or 
'massively-sophisticated-validated-datastructure' it is likely that a 
type-check will notice, whether static or dynamic.

> 
> >The second concerns safety and is unrelated to types.
> 
> Yeap.

Exception:  Pascal did its array bounds check as part of its 
integer subtyping system.  Not that its fixed-range arrays waere 
adequate for much real life, though.

> 
> >I don't really understand the third, but it seems like they're
> >conflating issues with integer overflow and unsafe casts.  The former
> >is an implementation property.  The later is an unsound type system.

This is why you still need bounds checks on integer operations -- in 
this case checks that the results fit inside the usual 8- or 16- or 32- 
or whatever integer representation.  There are situations where 
operations modulo 2^32 or such do the right thing, but there are many 
where it doesn't.  But the modulo integers are the ones C provides.
This on one place where the dynamically-typed languages can do it right 
by default by automatigically going to multiple-precision 
arithmetic.  They pay very little additional cost for this 
-- but only because the cost has already been paid by 
choosing the dynamically-typed language.
> 
> 
> Huh? There is nothing unsound about (String)10 or (double)10 or vice  
> versa. It's by definition a run-time conversion of bits, i.e., it is  
> functionality. So it belongs into the model side of the world and is  
> true -- by definition.
> 
> As the document says, it's all about overflow, underflow, ranges,  
> intervals, and missing checks. You may recall Pascal and its type  
> distinction of integers belonging to the range 1..10 and 1..20. You  
> needed to write a sort routine for each range. And that became a pain  
> you know where quickly. Otherwise I know no practical type system for  
> dealing with this.

Pascal lacked any mechanism for types that depended on variables.  The 
compiled-in bounds were unacceptable.  Later development of the Pascal 
standard introduced mechanisms for dynamic arrays, but probably lost the 
static bounds chacking (anyone know for sure about this?) 
> 
> Xi and Pfenning are doing research on what they call 'dependent'  
> types in this spirit. This is probably the best possible approach at  
> the moment, but it is much closer to soft typing (type check, eh,  
> theorem prove what you can, compile the left over claims into run- 
> time checks) than static typing. (Of course, it is a gray-scale.)

I always was a grey scale, as the possibility of the static type
'Dynamic' or 'Any' indicates.  Implementing dependent types without 
implementing them as 'Dynamic' or 'Any' is difficult.

> 
> >I think this is weak evidence that the presence or absence of a static
> >type system (of the sound, er, type) is unrelated to major security
> >holes.  The evidence is weak due to unsophisticated PLs used to
> >implement the vast majority of the programs out there, and the
> >inability to account for programming style (you can program Fortran in
> >any language, or so the saying goes).
> 
> Exactly. And that's why the discussion will go on. Of course, one  
> could also say that it is strong evidence and that the majority of  
> people are unwilling to accept because it contradicts the prevailing  
> dogma of "static types are good."
> 
> My opinion is that static types can play a useful role at several  
> stages of program design but that security is not one of them. And  
> won't be one for a couple of decades to come. Types are oversold  
> because academics can easily write a ton of papers on them without  
> implementing them and because -- like algorithms -- academics can  
> establish a pretty stratified hacking order using such papers. This  
> is a self-feeding process and there is little that will stop this.  
> Until it is so irrelevant that not even NSF will fund it.

As an academic, long ago, I tried working on dynamic types, and I 
insistedn on implementing them to test whether they would really work 
in practice.  I'm really weary of everything being done in principle 
and nothing in practice.  The result was a dearth of papers,  which 
ended my academic career and thus denied me the time and resources I 
needed to continue implementing them.  This was back in the 80's

Perhaps I was too obsessive-compulsive about implementing the 
concepts.  Or maybe there has to be a better way of running the world.

-- hendrik