Re: Spirit rover OS problems ( a reliable language )

From: Kelly Hall (hall_at_priest.com)
Date: 02/17/04 

Date: Tue, 17 Feb 2004 07:33:32 GMT

"Scott Moore" <samiam@moorecad.com> wrote in message
news:5v0Xb.168771$U%5.787137@attbi_s03...
> No, it cannot find this out all the time. It is not a %100 solution.
> Type safe languages are a %100 percent solution.

I'm not sure I understand you. The following code is type-safe but
doesn't work:

float sqrt(float x) {
  return -1.0;
}

There are certainly better, richer type systems out there, like
dependent types and subtypes. An issue with that is once you make the
type system rich enough to specify useful things, then it becomes
difficult or impossible for the compiler to automatically decide if the
types are right. In one environment I use that allows subtyping, you
may have to provide proofs to the system to allow it to accept your
code.

Personally, I'm a big fan of good type systems. But as long as users
want the convenience of automatic type checking then the type systems
will have to be sufficiently simple that they can't express much in
terms of overall correctness.

Kelly