[mercury-users] Native garbage collector for Mercury

[Randall Helzerman]

> 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).

> (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.

> > Moreover, once the
> > operating system is written in a pure logical programming language, we
> > could begin to think about things like _formally_proving_ that the OS
> > is secure.
> 
> Well, there is the halting problem. That aside, what you've just
> suggested is not a real time problem, but a security/accounting one.

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.

> 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
> 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 :-)