[mercury-users] Circular lists

[Richard A. O'Keefe]

    Thomas Charles CONWAY <conway at students.cs.mu.oz.au> wrote

	With all this talk of circular lists, I thought people might be
	interested/amused by the following.

	Beware, it is a complete hack, but IMHO quite cute.

We've seen quite a few examples recently of how Mercury's C interface can be
used to do strange and terrible things.  I keep on telling people that one
of the reasons special-purpose languages can be such a productivity boost
is not what they make it _easy_ to do but what they make it _impossible_ to
do; what classes of possible bugs are completely eliminated by construction
so that you don't have to spend any time at all looking for them.

Thomas Conway has just shown us how Mercury's C interface can be used to
subvert Mercury's compile-time termination verification.  That's not what
he meant it for, of course, but that is one (and not the worst) of its
effects.

I'm not into _forcing_ people to do what's good for them, but when using
Mercury I would very much like to know for certain that nothing of the
sort was going to affect my code.  Mercury is supposed to provide me with
speed AND safety.

Now the Quintus Prolog foreign interface was designed with the view that
the main use for such an interface was to access _existing_ libraries
(Fortran, Pascal, C &c), NOT to extend or change Prolog.  My slogan was
"the foreign interface is a crook, so the Prolog shepherd can lift up
the C sheep, not a crutch, for a strong C to prop up a weak Prolog".  
Foreign code had no access to Prolog data structures, and the only control
effects possible were to return, fail, or raise an exception.

That kind of interface _can't_ destroy the safety properties of a language
like Mercury, and to be frank, that's the kind of interface I really want.

Again, I'm not into forcing people to do what's good for them.
But I would like to _know_ that they have done what's good for _me_.
So,

    +---------------------------------------------------------+
    | Is there some tool that can be used to verify that the  |
    | Mercury foreign interface has been used in a useful but |
    | disciplined way that CAN'T break Mercury's type system, |
    | mode system, termination verification, or other safety  |
    | features?                                               |
    +---------------------------------------------------------+