[mercury-users] Native garbage collector for Mercury

[Philip Dart]

> Mercury's termination analysis is not very good at all.  OK it can
> prove termination for 50% of the compiler, but that still leaves about
> 50,000 lines of code to be proven terminating by hand.  Even with a
> 99% hit rate (which would be very hard to achieve), that's still about
> 1000 lines of code left for hand checking.  And unless you check it
> all (automatically or otherwise), the analysis is pretty much a waste
> of time since the answer to the question "Does this query terminate?"
> is still "Don't know".
> 
> This is not a slight against Mercury - the strong types and modes do
> come in very handy for proving termination - I just think that
> automatic termination analysis has a long way to go before it can be
> used for "real" programs in the way you suggest.

This argument also tells us why we shouldn't use a spell-checker, at least
not for real documents, until it can detect _every_ spelling mistake.
Tools like spell-checkers and termination analysers can increase our
level of confidence in documents/programs without proving the absence
of errors. Even though the question "Does this query terminate?" still
has the answer "Don't know", there are other questions such as "How much of
my program do I need to look at to work out why this query didn't terminate?"
that have different answers after termination analysis.

Philip

-- 
Philip Dart                             E-Mail: philip at cs.mu.OZ.AU
Department of Computer Science          Telephone: +613 9344 9103
The University of Melbourne             Facsimile: +613 9348 1184
Parkville, Vic 3052, Australia          WWW: http://www.cs.mu.oz.au/~philip/