Re: [Caml-list] Q: safe language

[didier plaindoux <didier@fecit.fr>]

[-- Attachment #1: Type: text/plain, Size: 4578 bytes --]


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

[-- Attachment #2: Type: text/enriched, Size: 5043 bytes --]


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


<excerpt>On Fri, 2002-08-30 at 14:44, Vitaly Lugovsky wrote:

<excerpt>On Fri, 30 Aug 2002, SooHyoung Oh wrote:


<excerpt>I heard Ocaml is "safe" language.


Some questions about "safe" language:

- Is it necessary for a safe language to have a type system?

</excerpt></excerpt>

<<...>


<excerpt> (cadr '(1))

</excerpt>

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

</excerpt>

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)

<bold><italic>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.</italic></bold><fontfamily><param>Times New Roman</param><bigger><bigger>

</bigger></bigger></fontfamily>

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)

<bold><italic>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
<underline><color><param>0000,0000,FFFF</param>unsafe
features</color></underline> 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</italic></bold><fontfamily><param>Times New Roman</param><bigger><bigger>. </bigger></bigger></fontfamily>


So you have two separated properties : type-safety (static or dynamic)
and runtime-safety (dynamic !). 

For example you can use OCaml unsafe features :


<fontfamily><param>Courier</param>	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


</fontfamily>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