[mercury-users] C Interface (was Circular lists)

[Tyson Dowd]

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 #