Re: [OT] Generalizing Types as Provable Invariants

[Matthias Felleisen <address@hidden>]

Yes, there are degrees of safety. But there are borderlines that 
are obvious. Or, as some Supreme Court Justice once said, "I know
it when I see it" though that wasn't about safety. -- Matthias


At 01 Jun 2002 02:49:09 +0200, Pixel wrote:
> Matthias Felleisen <matthias@ccs.neu.edu> writes:
> 
> > A type system for an unsafe language is insidious. -- Matthias
> 
> (troll below:)
> 
> ah, what is safe, what is not...
> 
> C, C++?  easy unsafe!
> 
> OCaml?
>   # let rec fact n = if n = 0 then 1 else n * fact(n-1);;
>   # fact 100;;
>   - : int = 0
>   hum, no warning, no error, no exception. Is that safe?
> 
> MzScheme?
>   > (- (+ 1 1e-100) 1)
>   0.0
>   hum, no warning, no error, no exception. Is that safe?
> 
> 
> the conclusion is of course not that all languages are the same!
> 
> 
> PS: I agree I had some problem making MzScheme fail since it has
> bigrats... but MzScheme allow simple things like "sqrt", opening the
> door to floating point... so even without using 1e-100 which is
> explictly a float (and not a bigrat), one can make the bad floating
> point underflow happen...