On Friday, August 30, 2002, at 03:05 PM, David Frese wrote:

> On Fri, 2002-08-30 at 14:44, Vitaly Lugovsky wrote:
>> On Fri, 30 Aug 2002, SooHyoung Oh wrote:
>>
>>> I heard Ocaml is "safe" language.
>>>
>>> Some questions about "safe" language:
>>> - Is it necessary for a safe language to have a type system?
>
> <...>
>
>>  (cadr '(1))
>
> This shows that Lisp is safe, because it results in an error, and does
> not return some value from out of nowhere (or does it).

In ocaml the result is :
	
Exception: Failure "hd"

But if you write (cdar '(1)) the corresponding ocaml code is not 
accepted by
the type checker :

Characters 9-20:
   List.tl (List.hd [1]);;
            ^^^^^^^^^^^
This expression has type int but is here used with type 'a list

This highlight a data type manipulation error ... It does not concern 
language safety
but only language type-safety.

In OCaml safety definition is : (cf. 
http://caml.inria.fr/FAQ/general-eng.html)
Caml is a safe language. The compiler performs many sanity checks on 
programs
before compilation. That's why many programming errors cannot happen in 
Caml:
data type confusions, erroneous accesses into compound values become just
impossible. In effect, all these points are carefully verified by the 
compiler, so that
the data accesses can be delegated to the compiler code generator, to 
ensure that
data manipulated by programs may never be corrupted: the perfect 
integrity of data
manipulated by programs is granted for free in Caml.

This definition only introduces static checks done by the compiler not 
the runtime ones.
You can design a language with a powerful type checker but without 
specific mechanisms
when you are in the "delta rules" layer (Try to write a extension for 
OCaml in c and forget
memory management ... You quickly have a core dumped).

Safety definition for Modula is : (cf. 
http://research.compaq.com/SRC/m3defn/html/complete.html#idx.17)
A language feature is unsafe if its misuse can corrupt the runtime 
system so that further
execution of the program is not faithful to the language semantics. An 
example of an unsafe
  feature is array assignment without bounds checking: if the index is 
out of bounds, then an
arbitrary location can be clobbered and the address space can become 
fatally corrupted.
An error in a safe program can cause the computation to abort with a 
run-time error message
  or to give the wrong answer, but it can't cause the computation to 
crash in a rubble of bits.

Safe programs can share the same address space, each safe from 
corruption by errors in the
others. To get similar protection for unsafe programs requires placing 
them in separate address
spaces. As large address spaces become available, and programmers use 
them to produce
tightly-coupled applications, safety becomes more and more important.

Unfortunately, it is generally impossible to program the lowest levels 
of a system with complete
safety. Neither the compiler nor the runtime system can check the 
validity of a bus address for
an I/O controller, nor can they limit the ensuing havoc if it is 
invalid. This presents the language
designer with a dilemma. If he holds out for safety, then low level code 
will have to be programmed
in another language. But if he adopts unsafe features, then his safety 
guarantee becomes void
everywhere.

The languages of the BCPL family are full of unsafe features; the 
languages of the Lisp family
generally have none (or none that are documented). In this area Modula-3 
follows the lead of Cedar
by adopting a small number of unsafe features that are allowed only in 
modules explicitly labeled
unsafe. In a safe module, the compiler prevents any errors that could 
corrupt the runtime system;
in an unsafe module, it is the programmer's responsibility to avoid them.

So you have two separated properties : type-safety (static or dynamic) 
and runtime-safety (dynamic !).
For example you can use OCaml unsafe features :

	Objective Caml version 3.06

# let f = Array.create 1 (fun x -> x) ;;
val f : ('_a -> '_a) array = [|<fun>|]
# Array.unsafe_set f 2 (fun () -> ()) ;;
- : unit = ()
# f ;;
- : (unit -> unit) array = [|<fun>|]
# Array.unsafe_get f 2 ;;
- : unit -> unit = <fun>
# (Array.unsafe_get f 2) () ;;
Bus error

But in this case we use unsafe features ... so we must keep in mind such 
program can crash !
This simple case highlights the type-safety and runtime-safety 
separation. So what is safety
now ? In OCaml type-safety is always verified but runtime-safety is 
implied by functions used
in applications ...

Didier