From: didier plaindoux <didier@fecit.fr>
To: Caml-list <caml-list@inria.fr>
Subject: Re: [Caml-list] Q: safe language
Date: Fri, 30 Aug 2002 17:28:30 +0200 [thread overview]
Message-ID: <23B5B988-BC2D-11D6-B235-00039301B6A4@fecit.fr> (raw)
In-Reply-To: <1030712751.1831.25.camel@pc-6>
[-- 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
next prev parent reply other threads:[~2002-08-30 15:29 UTC|newest]
Thread overview: 21+ messages / expand[flat|nested] mbox.gz Atom feed top
2002-08-30 1:36 SooHyoung Oh
2002-08-30 8:41 ` sebastien FURIC
2002-08-30 12:44 ` Vitaly Lugovsky
2002-08-30 13:05 ` David Frese
2002-08-30 13:46 ` Oleg
2002-08-30 16:09 ` Yutaka OIWA
2002-08-30 13:49 ` Vitaly Lugovsky
2002-08-30 14:04 ` J Farrand
2002-08-30 14:26 ` Vitaly Lugovsky
2002-08-30 14:48 ` Nicolas Cannasse
2002-08-30 15:31 ` Vitaly Lugovsky
2002-08-30 14:55 ` Mike Lin
2002-08-30 14:58 ` Eric Newhuis
2002-08-30 16:03 ` Yutaka OIWA
2002-08-30 21:44 ` Oliver Bandel
2002-09-01 8:07 ` John Max Skaller
2002-08-30 14:50 ` David Frese
2002-08-30 15:38 ` Vitaly Lugovsky
2002-08-30 15:28 ` didier plaindoux [this message]
2002-08-30 14:41 ` Florian Hars
2002-08-30 14:42 ` Nicolas Cannasse
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=23B5B988-BC2D-11D6-B235-00039301B6A4@fecit.fr \
--to=didier@fecit.fr \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox