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

[Richard A. O'Keefe]

	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.

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.

You might be surprised at just how checkable (new) C code can be.

	Perhaps we have different ideas on what is checkable from such a tool,
	and how large that checkable set needs to be before it is useful.

Exactly.  The Mercury team seem to have jumped to the conclusion that I meant
some kind of universal theorem prover that could just about write the programs
for you, whereas I want something much more modest:  a list of safe interface
features and a tool that checks that only those features are used.

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.

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.