[Prev][Next][Index][Thread]

Re: type safety


Sorry Bob, but IMHO this message doesn't contribute much to the
discussion. I think people have this much of the picture in mind.

Indeed, it is straight out of a paper that Shriram and I submitted in 97
and that we turned into a tech report last year. I have placed it in a tmp
web directory for people's perusal:

  http://www.cs.rice.edu/~matthias/Tmp/safe.ps

The paper is an attempt at formulating what I have called data and memory
safety over the years. (I am happy to admit that the paper has flaws and 
needs improvements.)

Even the claim that 

     "C is safe" 

is anticipated in the paper. We can study real C or a theoretical C. 
If we study theroetical C, we should include array mis-referencing. 
In that case, the (abstract) machine can either index beyond the end of 
the array or, as you say, perform an error transition. In the first case,
you have an unsafe C; in the second one, you have a safe C -- except that
you have only one class of data (numbers). 

We can also study real C, which is a thin veneer over the machine +
Unix. This "language" (as Matthew Flatt and Greg Morrisett pointed out in
private messages) is safe and deals with one kind of data: pages. If the
program=process indexes into a bad page, the machine raises an exception,
called a seg fault or a bad memory access etc. [Of course, pages aren't
 accessible in C but through asm, which stands in for the machine's
 language, so abstraction isn't obtainable in C per se.]

In either case, the language has one class of data. As I have said in a
previous message, safety is a spectrum. I believe that safety for languages
with one form of data is a pointless exercise. Just as a one-point model
for the pure Lambda-calculus is a useless exercise. The challenge is to
enforce separation between classes of data and to make some of the program
operations in a language partial (they fault). 

-- Matthias