[mercury-users] Native garbage collector for Mercury

[Ralph Becket]

Randall Helzerman wrote on 10 Sep:
> > Robotics (et al.) is a different kettle of fish.  The key problems with
> > higher-level (declarative) languages in this field are
> 
> Actually, logic programming has many advantages for use in robotics, and is
> really being used. (check out Miller and Shanahan's project at
> http://www.dcs.qmw.ac.uk/~mps/CogRob/CogRob.html for example).

I've just taken a look at Shanahan's web page and I get the impression
that his field (like mine) is planning as theorem proving.  I'll have
to look more closely at his papers when I have more time, but the gist
of it seems to be that he is applying classical planning techniques to
robotics.  The trouble with planning technology is that, in general,
it is trying to solve an intractable problem.  Plan space is
unbelievably large in interesting domains.  As I say, I'll have to
read more, but I'd be *extremely* surprised if any mission-critical
deep planning is going on in real-time here.  Contemporary planners
just ain't good enough.

> > (iii) there is no obvious mapping from the declarative language to the
> > underlying hardware, which is a major feature of hard real time
> > systems.
> 
> I'd have to disagree with you there; the declarative programming paradigm
> coupled with the event calculus can provide very intuative and natural 
> mappings for both high and low-level events.  In fact it is particularly
> good at keeping track of hierarchical events and planning.  Again, check
> out Shanahan's page above for more info.

Maybe we're talking at cross purposes here.  I think you're saying
that declarative languages are good at modelling systems, in which
case I agree with you completely.  The point I was making was that the
low-level code that gets generated by a declarative language compiler
for any given line of source code often has very little recognisable
connection with the original source: one of the reasons declarative
languages work is because you can apply heavy-weight optimisation at
several different levels.  In C this is not quite the case - for any
expression/assignment/array reference etc. you have a fair idea of
what sort of assembly is going to be generated.  This really can make
a difference in high-performance parts of an operating system.

> So Ralf, part of your research is software agents, right?  My point is this:
> Right now there are several attempts to define an "agent language" such as
> KIF or KDE for purposes of communications/marshelling of resources in
> distributed computing.  Instead of starting from scratch to create a
> new agent modeling language, I believe that it would be a better strategy
> to use Mercury as a starting point--with its termination analysis capability
> being a big selling point.  Yes, there's the halting problem, but Mercury's
> termination analysis is already very good (it can prove the termination of
> over 50% of the proceedures used in the Mercury compiler, for example), and
> there's nothing which prevents someone from writing a server which will only
> run programs which Mercury can prove will terminate.

[My web page is a bit out of date - I've been doing planning for
wayyyy too long now...]  Isn't this changing the debate somewhat?  The
point I was originally arguing concerned (hard) real time systems.  As
for "agent languages" I'm a bit sceptical and it's a whole other can
of worms.  Another time!

> > There is also the problem that many formal spec. jobs end up (after a
> > great deal of work) showing that the original spec. was flawed. 
> 
> Dude, do you know how many CPU cycles we're burning up right now doing
> formal verification for Merced?  Yes of course, the original spec might be
> (and often is) flawed, but finding that out is a feature and not a bug of
> formal verification.  Formal verification is the hottest thing going right
> now in VLSI CAD.  What prevents it from being the hottest thing in software
> is that the hottest language in software is C++.  If everybody were
> programming in a pure language like Mercury, it would be a giant enabler for
> formal verification methods in software engineering.

I'm all in favour of formal methods and their development, I was just
trying to bring things down to Earth a little!  I would argue that
software systems are more complex than the hardware they run on.  But
you have a point - God forsaken languages like C++ don't help much.

> > I would have thought that a real OS would be way beyond the
> > current state of the art, either in terms of defining a spec. or
> > turning such a spec. into an efficient program.
> 
> We're researchers, our job is go go beyond the state of the art :-)

To boldy go...

-- 
Ralph Becket  |  rwab1 at cam.sri.com  |  http://www.cam.sri.com/people/becket.html