No subject

[Fergus Henderson]

Return-Path: <trd at mundook.cs.mu.OZ.AU>
Received: from mundook.cs.mu.OZ.AU by mulga.cs.mu.OZ.AU with SMTP (5.83--+1.3.1+0.51)
	id AA18144; Fri, 28 Nov 1997 14:02:02 +1100 (from trd at mundook.cs.mu.OZ.AU)
Received: (from trd at localhost) by mundook.cs.mu.OZ.AU (8.8.5/8.7.3) id OAA15861; Fri, 28 Nov 1997 14:02:01 +1100 (EST)
Message-Id: <19971128140201.46199 at mundook.cs.mu.OZ.AU>
Date: Fri, 28 Nov 1997 14:02:01 +1100
From: Tyson Dowd <trd at cs.mu.oz.au>
To: mercury-users at cs.mu.oz.au
Subject: Re: [mercury-users] C Interface (was Circular lists)
References: <199711270810.TAA26632 at goanna.cs.rmit.edu.au>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Mailer: Mutt 0.88
In-Reply-To: <199711270810.TAA26632 at goanna.cs.rmit.edu.au>; from Richard A. O'Keefe on Thu, Nov 27, 1997 at 07:10:14PM +1100
Status: O
Content-Length: 4266
Lines: 86

On 27-Nov-1997, Richard A. O'Keefe <ok at cs.rmit.edu.au> wrote:
> 	Merely defining _checkable_ code and devising algorithms to check such
> 	code sounds like a fairly substantial project.
> 
> 	It sounds like you'll be pretty much restricted to checking what
> 	could be called "pure C". But "pure C" doesn't let you do anything you
> 	can't do in Mercury anyway. We *need* the C interface to do things like
> 	I/O, networking, IPC, graphics, pointer-manipulation, etc. 
> 
> This is a straw man.  You are attacking something I am not proposing.
> How many times do I have to say that I accept that if the foreign code
> breaks the rules of the foreign language, all bets are off?
> What I'm asking about is whether there is or could be `middle-level'
> *interface* where safe use of the *INTERFACE* can be checked on the
> assumption that the rest of the foreign code is doing legal things according
> to the rules of the foreign language.

And I have proposed that it would be a good course of action to create
(or enhance) the C interface so that it can provide an environment where
you can't do anything but be correct (except if you break the rules
of the foreign language). So the C compiler can tell you if you are 
breaking the rules. It would then be relatively easy to invoke the C
compiler with all warnings enabled in the code that someone else writes.

We already do some static checks of C code (the names of all the input
and output variables must be mentioned in the C code). Checks of this
nature would be OK to do, but I don't think anyone is willing to parse C
code to find out whether you are doing something unsafe. From your
first posts it sounded like this is what you wanted, but I think you
were just being terse.

> The Quintus interface, with *NO* access to Prolog data structures or control
> from C, was entirely adequate to do I/O, networking, IPC, &c.  I believe a
> lower level access *to C structures* was provided to Prolog about the time
> I left.  Peter Schachte can comment on this, because he implemented it.
> But Prolog access to C data structures is not the same as C access to
> Prolog data structures.
> 
> What I'm getting at is really incredibly simple:  a subset of the interface
> that can be used to pass some subset of *C* data structures between Mercury
> and C, where an amazingly simple tool can say "yes, you have used no
> interface features outside that subset".
> 
> You can do _all_ of I/O, networking, IPC, and graphics with an interface
> subset like that.
> 
> 	The other thing we need the C interface for is accessing large libraries
> 	of pre-written code, and it's almost certain that any large amount of
> 	code will not be checkable.
> 
> Again, that's because you are talking about checking everything the foreign
> code is doing, while I was only asking that safe use of the INTERFACE be
> checked.  And by "checkable code", I meant code where THAT check is easy,
> and all I meant was using suitably crafted macros instead of powerful
> primitives.

I don't know why it looks like we are arguing. Except for the details,
we seem to be in compelete agreement. I think calling it a 'tool' made
it sound like you wanted a theorem prover. If this was our
misunderstanding, then we'll let it die now.

> Yes, it will still be possible for foreign code to do arbitrary damage
> IF it breaks the foreign language rules, but I was never asking for arbitrary
> code checks, only interface checks.  The point is to check that nobody is
> _deliberately_ doing dangerous things without leaving bright flashing warning
> signs nearby.

Well, the other possiblity for leaving warning signs is to use `impure'
declarations (which are being worked on). These would allow you to
write Mercury code that relies on C code that is impure, but eventually
when you put enough of the code together, it is pure.

> I've got to leave this thread because I'm catching a plane on Saturday and
> leaving Melbourne permanently.  I'll be off the air until January.

That's cheating. You can't leave a thread dangling like this!

-- 
       Tyson Dowd           # 
                            #         Linux versus Windows is a 
     trd at cs.mu.oz.au        #            Win lose situation.
http://www.cs.mu.oz.au/~trd #