Re: [Caml-list] GC and file descriptors

[skaller <skaller@ozemail.com.au>]

On Wed, 2003-11-19 at 09:23, Brian Hurt wrote:
> On 19 Nov 2003, skaller wrote:

> The fact that it's insolvable means that the language can not issue 
> blanket gaurentees, just "best effort" requirements.  Which work fine 
> right up until the point that the best effort fails.

That isn't the way I'm looking at it. Let me try to explain
better. Consider you have a general case and some subclass
of the problem which is easily solvable.

What you do is restrict the language to the subclass:
the general case is not useful precisely because
it is incomprehensible, meaning you cannot easily
form judgements about it.

I want to give a real example of this.
We all know that proving an arbitrary
program terminates is impossible, where
the programming system is Turing complete.

My point is: who cares?? We clearly do NOT
need Turing complete programming systems,
because the behaviour is unpredictable.
Programs are meant to have predictable
behaviour.

So you just restrict the language so
that you CAN prove with some algorithm
that every program terminates (or not).

Oh yes, it has been done, and the language
is very powerful (though not Turing complete).

See Charity: all Charity programs
terminate. True, some things you can
write in Ocaml cannot be expressed in Charity.

Also true: some things you can write in Python
cannot be expressed in Ocaml (because the type
system is not expressive enough whereas Python
doesn't care).

Yet, Ocaml is still useful for a large class
of problems .. and one really has to push
hard to find an application where the full power
of dynamic typing is really needed.

So I think really the issue here is trying to
find a compromise between the ability to reason
about something and the ability to express it:
if the constraints are too tight reasoning is
easy but irrelevant because you cant solve any
problems, and if it is too expressive you can't
reason and also cannot solve problems [in the sense
that whilst the program appears to work you 
don't have any assurances from the system it will]

Of course that balance is found by research,
and new results allow the frontier to be pushed.
In the case of Ocaml there is a strong emphasis
on the type system as a means of constraining
code [the aim is not to be sure the code works,
but to gain *some* reasonable assurance -- in practice
Ocaml strong typing is extremely good
at predicting when my programs will work -- if it
compiles it either works immediately of has
only a few bugs in it]



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