Re: [OT] Generalizing Types as Provable Invariants

[Pixel <address@hidden>]

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