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.Times New Roman
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
0000,0000,FFFFunsafe
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
themTimes New Roman.
So you have two separated properties : type-safety (static or dynamic)
and runtime-safety (dynamic !).
For example you can use OCaml unsafe features :
Courier Objective Caml version 3.06
# let f = Array.create 1 (fun x -> x) ;;
val f : ('_a -> '_a) array = [|<|]
# Array.unsafe_set f 2 (fun () -> ()) ;;
- : unit = ()
# f ;;
- : (unit -> unit) array = [|<|]
# Array.unsafe_get f 2 ;;
- : unit -> unit = <
# (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