[Caml-list] Q: safe language

[Caml-list] Q: safe language

[SooHyoung Oh]

I heard Ocaml is "safe" language.

Some questions about "safe" language:
- Is it necessary for a safe language to have a type system?
- Isn't Lisp a safe language?
 
---
SooHyoung Oh
tel: 02)583-8709, 042)861-8649
cell. phone: 011-453-4303
web: http://www.duonix.com


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[sebastien FURIC]

SooHyoung Oh a écrit :
> 
> I heard Ocaml is "safe" language.
> 
> Some questions about "safe" language:
> - Is it necessary for a safe language to have a type system?

 Typing ensures the functions to be applied the right way. So a safe
language must be typed, either dynamically (like LISP) or statically
(like O'Caml).

> - Isn't Lisp a safe language?

 You can consider it as a degenerated version of O'Caml with only one
type (object):
type object =
   | Integer of int
   | String of string
   | Cons of object * object
   | Nil
   ...
 Since functions (from objects to objects) can't fail (no core dump),
LISP may be considered as a safe language...

 Sebastien.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Vitaly Lugovsky]

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?
> - Isn't Lisp a safe language?

 (cadr '(1))


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[David Frese]

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?

I would say yes, and it definitely needs a strict type system (I guess
there is no language without a type system at all). Strict means: every
value has a precise type - which does not mean that there are no
polymorphic types, or type conversions.

> > - Isn't Lisp a safe language?

In that respect Lisp is a safe language - or at least Scheme; I don't
know that much about Lisp. But "safe" can be interpreted in a lot of
other ways of course.

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

David.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Oleg]

On Friday 30 August 2002 09:05 am, David Frese wrote:
> >  (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).

On Debian CMUCL it returns NIL.

BTW I'd rather have things like  (+ 3 "four") weeded out at compile time.

Cheers,
Oleg
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Yutaka OIWA]

>> On Fri, 30 Aug 2002 09:46:50 -0400, Oleg <oleg_inconnu@myrealbox.com> said:

> On Friday 30 August 2002 09:05 am, David Frese wrote:
>> >  (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).

> On Debian CMUCL it returns NIL.

In Common Lisp, the cdr of () is defined to be (). The car of () is also ().
I personally hate this definition :-(

# car x = car y, cdr x = cdr y, but x <> y
#                                if x = (()) and y = ()

-- 
Yutaka Oiwa              Yonezawa Lab., Dept. of Computer Science,
      Graduate School of Information Sci. & Tech., Univ. of Tokyo.
      <oiwa@yl.is.s.u-tokyo.ac.jp>, <yutaka@oiwa.shibuya.tokyo.jp>
PGP fingerprint = C9 8D 5C B8 86 ED D8 07  EA 59 34 D8 F4 65 53 61
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Vitaly Lugovsky]

On 30 Aug 2002, David Frese wrote:

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

 No. In this place program may be expecting some structure, which can 
contain NIL. There is no other way in lisp to define structures - so, any
code accepting lists will accept any alien structure. Is is type safety? 
No way! Dynamically typed languages can't be safe.



-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[J Farrand]

On Fri, 30 Aug 2002, Vitaly Lugovsky wrote:

>  No. In this place program may be expecting some structure, which can
> contain NIL. There is no other way in lisp to define structures - so, any
> code accepting lists will accept any alien structure. Is is type safety?
> No way! Dynamically typed languages can't be safe.

"Safe" is not the same as "Type Safe".  ISTR safe means that a program
written in the language will not cause a machine level error.  So for
example, C is not safe because you can derefence a bad pointer etc. and
cause a seg fault.  LISP is safe.  Even though you can apply a function to
arguments of the wrong type, LISP has well defined behaviour for dealing
with this.  (That behaviour might just be that the runtime prints an error
a halts the program, but still better than what C would do, which is
basically anything...)

--
Jim Farrand, ML Group,               mailto:farrand@cs.bris.ac.uk
Department of Computer Science,      http://www.cs.bris.ac.uk/~farrand
University of Bristol,               tel: +44-(0)117-954-5254
Woodland Road, Bristol, BS8 1UB, UK
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Vitaly Lugovsky]

On Fri, 30 Aug 2002, J Farrand wrote:

> >  No. In this place program may be expecting some structure, which can
> > contain NIL. There is no other way in lisp to define structures - so, any
> > code accepting lists will accept any alien structure. Is is type safety?
> > No way! Dynamically typed languages can't be safe.
> 
> "Safe" is not the same as "Type Safe".  ISTR safe means that a program
> written in the language will not cause a machine level error. 

 Ok, fixed. But I don't see any difference between segfault and NIL passed
as file descriptor. Program fails - and it does not matter, was it "low 
level" fault or unhandled exception or uncorrect behaviour.

> So for
> example, C is not safe because you can derefence a bad pointer etc. and
> cause a seg fault.

 Run C in a bytecode "safe" environment (there are some C implementations
with this functionality) - and it will become a "safe language"?

>  LISP is safe.

 Okee. Lisp execution environment is safe. Java execution environment is 
safe. C execution environment could be safe. But C is not a safe language,
as well as Java and Lisp.

>  Even though you can apply a function to
> arguments of the wrong type, LISP has well defined behaviour for dealing
> with this. 

 And C runtime environment can have a well defined behaviour of what to do 
with wrong pointers.


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Nicolas Cannasse]

> > So for
> > example, C is not safe because you can derefence a bad pointer etc. and
> > cause a seg fault.
>
>  Run C in a bytecode "safe" environment (there are some C implementations
> with this functionality) - and it will become a "safe language"?

True.
If you choose the following definition "safe : which does not fail" then you
have

C < "safe" C < Lisp < OCaml

But you can't ensure the total safety of your program without using a
theorem prover such as COQ.
Simple OCaml sample :

List.hd [];;

Nicolas Cannasse

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Vitaly Lugovsky]

On Fri, 30 Aug 2002, Nicolas Cannasse wrote:

> >  Run C in a bytecode "safe" environment (there are some C implementations
> > with this functionality) - and it will become a "safe language"?
> 
> True.
> If you choose the following definition "safe : which does not fail" then you
> have
> 
> C < "safe" C < Lisp < OCaml
> 
> But you can't ensure the total safety of your program without using a
> theorem prover such as COQ.
> Simple OCaml sample :
> 
> List.hd [];;

 [] is a correct argument for hd, but list (x y) is not a correct when 
you're expecting 3-d vector (x y z). So, well, I don't see the difference
between "safety" and "type safety".


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Mike Lin]

>  Ok, fixed. But I don't see any difference between segfault and NIL passed
> as file descriptor. Program fails - and it does not matter, was it "low 
> level" fault or unhandled exception or uncorrect behaviour.

It makes a big difference if you're running in a realtime system with a
shared memory model.

>  Okee. Lisp execution environment is safe. Java execution environment is 
> safe. C execution environment could be safe. But C is not a safe language,
> as well as Java and Lisp.

The meaning of "safe" is completely nebulous here. Type safety is
provided very well by OCaml. But then we have things like

# max_int;;
- : int = 1073741823
# max_int + 1;;
- : int = -1073741824

Obvious performance and practicality concerns preclude checking the
bounds on every addition operation. Nonetheless, this could without much
stretch of the imagination be called "unsafe". 

-Mike

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Q: safe language

[Eric Newhuis]

One might define compile-time safety as the ability to enforce rules at
compile time.  All the better if the programmer can establish the rules.
One person's safety is another person's barrier.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Yutaka OIWA]

What a hot topic for me! :-)

>> On Fri, 30 Aug 2002 18:26:07 +0400 (MSD), Vitaly Lugovsky <vsl@ontil.ihep.su> said:

Vitaly> On Fri, 30 Aug 2002, J Farrand wrote:

Vitaly>  Ok, fixed. But I don't see any difference between segfault and NIL passed
Vitaly> as file descriptor. Program fails - and it does not matter, was it "low 
Vitaly> level" fault or unhandled exception or uncorrect behaviour.

No. SIGSEGV?  You are lucky.

You got SIGSEGV because an invalid pointer luckily points to the
outside of the process boundary. If it points to the inside of the
process, anything can be occur.  SIGSEGV, Malicious code injection,
clearing all your files, formatting your harddisk if you are a root,
and whatever else.

# SIGSEGV can be thought to be "safe" or "handled" if it is
# caused strictly by dereferencing "NULL" (or zero) in Unix environment.
# But many SIGSEGV are caused by buffer-overrun, dangling pointers, etc.
# Those are not safely handled.

The LISP exception you called it "unhandled" is actually handled.
It halts the program execution without relying to any luck.
It is defined to be so.

>> So for
>> example, C is not safe because you can derefence a bad pointer etc. and
>> cause a seg fault.

Vitaly>  Run C in a bytecode "safe" environment (there are some C implementations
Vitaly> with this functionality) - and it will become a "safe language"?

Yes.

If there is no free(), no pointer arithmetic, no casting, no buffer overflow,
it is OK.
Malloc-free problem can be solved by GC.
Buffer overflow?  Check the boundary like Java.
Pointer arithmetics?  Use fat pointers.
Pointer cast (to/from void*)?  Hmm... but it can be done.

I and many other people are working on this problem.


But, we must be aware, if we say "C language is not safe", or
"Scheme is type-safe", we assume some "normal" implementation
of the language.  If we pass "-unsafe" option to ocamlc, it becomes
unsafe.  A mini-Scheme compilers which Junior students in our
department wrote as an assignment does not check '() in cdr function and 
thus not type safe.  If you use our "Fail-Safe ANSI-C compiler"
(sorry not yet finished), C language becomes type-safe.
But you expected those tricky answers?  I think you don't.

# In addition, "safety" depends on its definition.
# If we assume a machine language which has only the type "word",
# and assume every machine state is "OK", then the machine language is
# "type-safe". But this is also not what we want.
# We must share some "normal" interpretation of the "safe" or
# "type-safe" states.

Vitaly>  And C runtime environment can have a well defined behaviour of what to do 
Vitaly> with wrong pointers.

In usual way of compilation, it is not possible. It requires
some heavy changing of the way of compilation, which most people
think "unusual".

-- 
Yutaka Oiwa              Yonezawa Lab., Dept. of Computer Science,
      Graduate School of Information Sci. & Tech., Univ. of Tokyo.
      <oiwa@yl.is.s.u-tokyo.ac.jp>, <yutaka@oiwa.shibuya.tokyo.jp>
PGP fingerprint = C9 8D 5C B8 86 ED D8 07  EA 59 34 D8 F4 65 53 61
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Oliver Bandel]

Hi,

On Fri, 30 Aug 2002, Vitaly Lugovsky wrote:

> On Fri, 30 Aug 2002, J Farrand wrote:
[...]
> >  Even though you can apply a function to
> > arguments of the wrong type, LISP has well defined behaviour for dealing
> > with this. 
> 
>  And C runtime environment can have a well defined behaviour of what to do 
> with wrong pointers.
[...]

Well, C (which means ANSI-C or ISO 9899-C) says nothing about
how your environment is behaving. There are a lot of holes
in the C-standard and these holes are "undefined behaviour",
"implementation dependent" and similar...


But I agree that integer-border-problems in Ocaml
are not very fine. This is a hole in Ocaml.

(But if known, you can handle it; there are much more
 holes in C than in Ocaml.)

Ciao,
   Oliver

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[John Max Skaller]

[long post ...]

J Farrand wrote:

> On Fri, 30 Aug 2002, Vitaly Lugovsky wrote:
> 
> 
>> No. In this place program may be expecting some structure, which can
>>contain NIL. There is no other way in lisp to define structures - so, any
>>code accepting lists will accept any alien structure. Is is type safety?
>>No way! Dynamically typed languages can't be safe.
>>
> 
> "Safe" is not the same as "Type Safe".  ISTR safe means that a program
> written in the language will not cause a machine level error.


It's a dubious distinction. I don't agree. Safe could mean
"guarranteed to be correct at compile time". Since there
certainly is no way to specify intended semantics in any language,
since even such a specification could be wrong,
"safe" as I just specified is a formally meaningless term.

>  So for
> example, C is not safe because you can derefence a bad pointer etc. and
> cause a seg fault.


That's wrong. There is no such requirement in the ISO C Standard.
Indeed, instrumented versions of C check for null pointer
dereferences. Some may do so with code inserted at each
dereference, and some by trapping hardware exceptions.
Solaris "Purify" is such an instrumenting program.

> LISP is safe.  Even though you can apply a function to
> arguments of the wrong type, LISP has well defined behaviour for dealing
> with this. 


Well definedness isn't enough either. Many things in C
are not "well defined", but they're not unsafe either.
The actions of a C language translator may have one
outcome (deterministic), one of several (which is called
"unspecified behaviour" in ISO C++), anything the implementor
defined ("implementation specified" in C++), or any
behaviour at all ("undefined behaviour" in C++).

It's not clear what "well defined" means, when one
simply says that the behaviour of any program
is one of a set of behaviours, possibly a singleton
(deterministic) or possibly the universal set
("undefined") -- that makes the behaviour
"well defined" in all cases!

Even a syntax error has well defined behaviour--
the translator is required to reject the program
and issue a diagnostic error message.
Note that the distinction between compile time
and run time doesn't exist for C or C++ (to allow
interpreters to be legitimate implementations),
so you can't start talking about "run time" failures.
Clearly, the Ocaml bytecode interpreter in interactive
mode is an interpreter too.

Of course, there is an urban myth that some languages

are "safe" and others are not. Ocaml, unfortunately,
contributes to this misleading idea by claiming
to be a "safe" language.

It isn't. It can core dump. It can throw exceptions.
It doesn't guarrantee correctness. It contains non-deterministic
semantics whose behaviour sets are restricted but not singleton
(such as bit operations on ints).

Perhaps you can say that Ocaml programs cannot
have a certain class of errors such as null pointer
dereferences, though that really an ill-formed
claim, since it doesn't have pointers :-)

A more important claim is that the type system is sound,
while that of, say, C++, is not. That is a proposition
of a formal mathematical system, although the formal
model of the typing of each language is not given
precisely (either in the C or C++ Standards, or in the
Ocaml reference). Still, this kind of claim has more
weight in my mind, than saying Ocaml is 'safer' than
C simply because it traps some addressing exceptions.

In my opinion, it is more useful to ask users
of multiple languages "in which language do you feel
that for a given budget and resources you can deploy
a program and expect the smallest maintenance costs?".

Now there, without hesitation, I'd place Ocaml well
above C++ for a considerable class of applications,
particularly the kind I like to develop :-)

I think the question is a good start,
because with some thought and assumptions one might
even *quantify* the answer: such a metric would
be problematic, but its existence might start to
give some credence to the intended notion:
that Ocaml is a better language because it is
cheaper to develop a robust application with a
given semantic/performance goal, for a significant
range of application types.

This is actually a Frequently Asked Question:
"Is Ocaml good for numerical programming?
Game programming?" so I think that it may be
a sensible measure of quality.

More abstractly, we ask: "What formal properties
are correlated with quality programming languages?"
with answers like "sound type system" and
"garbage collection" and "referential transparency"
all being accepted indicators. And one that
should be popular on this list "Strong emphasis
on functional programming style" :-)


---
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[David Frese]

On Fri, 2002-08-30 at 15:49, Vitaly Lugovsky wrote:
> On 30 Aug 2002, David Frese wrote:
> 
> > >  (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).
> 
>  No. In this place program may be expecting some structure, which can 
> contain NIL. There is no other way in lisp to define structures - so, any
> code accepting lists will accept any alien structure. Is is type safety? 

If you are refering to the fact, that the expression above returns NIL,
then yes, this is no type-safety, and a very bad thing - I did not know
that.

> No way! Dynamically typed languages can't be safe.

I don't think this is a problem of dynamic or static typing, but a mad
behaviour of Lisp.

BTW: I guess we're getting a little bit off-topic now.

David.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Vitaly Lugovsky]

On 30 Aug 2002, David Frese wrote:

> > > >  (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).
> > 
> >  No. In this place program may be expecting some structure, which can 
> > contain NIL. There is no other way in lisp to define structures - so, any
> > code accepting lists will accept any alien structure. Is is type safety? 
> 
> If you are refering to the fact, that the expression above returns NIL,
> then yes, this is no type-safety, and a very bad thing - I did not know
> that.

 It depends on the Lisp implementation. But, you can find a lot of 
"unsafe" examples with correct behavior: e.g. 3-d vector passed as 2-d 
vector, and lisp function working with structures using only cars and 
cdrs will not fail with it.

> > No way! Dynamically typed languages can't be safe.
> 
> I don't think this is a problem of dynamic or static typing, but a mad
> behaviour of Lisp.

 With polymorphism and dymanic typing the programm may not fail at the 
point where wrong type was passed - and this is "unsafe" behaviour (this 
is where I have an ugly headache with Java).
Statically typed language will not allow potentially unsafe function 
calls. 


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[didier plaindoux]

[-- 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

Re: [Caml-list] Q: safe language

[Florian Hars]

SooHyoung Oh wrote:
 > Some questions about "safe" language:
 > - Is it necessary for a safe language to have a type system?

Yes, but it needn't be static nor strong. Perl (like the other, less obfuscated
dialects of Lisp :-)) is a safe language, too: there is no way that the
execution of a valid instruction like an access of a variable will result in a
program crash, the only risk is an unexpected result if you miss some $ in
${$$r{$i}}[$j].

In C, on the other hand, it is perfectly possible to have a valid code fragment

   int * i_ptr;

   i_ptr = get_some_address();
   &i = 42;

that may occasionally crash.

 > - Isn't Lisp a safe language?

Yes, as Vitaly Lugovsky has convincingly demonstrated in another message.

Yours, Florian
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Q: safe language

[Nicolas Cannasse]

> I heard Ocaml is "safe" language.
>
> Some questions about "safe" language:
> - Is it necessary for a safe language to have a type system?
> - Isn't Lisp a safe language?

Depends what you're calling "safe"...

Any language having garbage collection prevents the user from having "access
violations" errors ( such as in C :  (*NULL)++ ). Then, other errors will
always be detected either at run-time ( with often an exception mechanism )
or at compile time.

Lisp is a dynamicly typed language, so will perform all type checks at
run-time, resulting a very simple way of writing things but most of the (not
syntax) errors will be detected by the user at run-time. This kind of
language require rought testing of the programs from the user ( keep in mind
that a runtime error is taking at least 10 more time to find/fix than a
compile-time one )

Then comes strongly types languages. Theses need "types" and will only
accept compiling programs where functions are applied to the good typed
parameters. Perhaps more work is needed by the programmer, but most of Lisp
run-time errors are now detected at compile-time, resulting a "more safe"
binary.

OCaml is far better than that, but it does "type inference" for you. That
is, it automaticly deduce variables & functions types from the context in
which they are used. So you can write programs with almost the same freedom
as Lisp ( without type anotations ) but with a compile-time errors-detection
:-)

Nicolas Cannasse

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners