[Gcl-devel] Re: Thanks

[Camm Maguire]

Greetings, and thank you so very much for this very informative and
helpful reply!

Robert Boyer <address@hidden> writes:

> In my opinion, in broad, practical outline, ML as a programming language is
> nothing but Lisp with your hands tied behind your back "for your own good."
> They make you type everything so extremely well that you do get a lot of type
> information.  But is it worth the cost?  Well, a lot of ML people think so.
> Someone ML enthusiasts have been known to claim that most of the mistakes
> they have ever made as programmer now get caught as type errors by
> ML!

I agree, from my very limited knowledge, that C type compile-time
type checking is definitely not a feature lisp should go chasing.  And
it seems that ML is somewhere between lisp and C on this score.  One
apparent advantage of lisp is its simple presentation of the logic
behind functions -- clutter must be reduced at almost all cost to gain
clarity of conception.  This is not to say that compilers should not
try to warn you whenever possible, but if one wants to design a
language to make this easier for the compiler, one might as well use C
IMHO.  

Personally, I find I can do just about whatever I want in C.  And
paradoxically, many errors do get caught by the compiler, but they are
almost always of the typo or silly oversight sort.  But the allure of
lisp is -- look what people have written in it!  While C attracts the
kernel writer, lisp definitely appears to attract the mathematician,
and this is reason enough to keep it going, IMHO.


> By far, the one extremely beautiful and scientifically important point about
> ML is that by using its type security, one can define as a "type" the idea
> theorem, and one can state one's rules of inference as producers of objects
> of said type, and then one can know by type security that one has code that
> only produces theorems.  (Call it object oriented programming circa 1971 with
> a security motive.)  Now, this is major, major, major, scientifically.  Take
> the case of Coq and the Four Color theorem.  In principle, their achievement
> is monumental because, since Gonthier did it in Coq, which is done in ML
> (OCAML, really), they are really sure they've got a proof, whereas if, say J
> Moore or Matt told you they had done the same in ACL2, you'd have to worry
> about whether there were bugs in ACL2 and that is a really large amount of
> code.  Of course, there can be bugs anywhere, and John Harrison (of HOL and
> HOL light), once told me that bugs were found later, after years, in the tiny
> innermost core of HOL, around lambda conversion, of course.
> 

I am intrigued by your very helpful description.  Do you have
online references on the idea theorem, and how this works in practice?
This sort of logical mapping of logic itself onto the programming
language would appear to be something very useful to lisp and the type
of applications for which it is typically used. 


> Now, Lisp could or may have a similar concept of type security that was
> mechanically checked by the type and runtime system, but I don't know for
> sure because Lisp itself, like a good experimenter's workbench, is so chock
> full of warts and wormholes that it is hard really to know.  Are there around
> instructions, like (setf (aref ..) ..) that when run with safety 0 allow you
> to smash absolutely anything?  Of course.  So can you stand to run with
> safety 3?  Hard to say?  

Hard for me to say too, so I am polling gcl-devel and particularly
Paul Dietz.  We have the rudiments of a thread going on good type
propagation algorithms in the compiler.  I'd most appreciate his
thoughts on the above.

> > Lastly, HOL88 built some sort of ML on top of akcl -- do you know why
> > that approach was abandoned?
> 
> I think that for a good while, that ML was the standard of all MLs!!!  And
> was dearly loved.  I think that it was never really abandoned except for
> performance reasons, which they seem to have gotten, with OCAML.  

You know, it might not be a bad idea to resurrect it in some kind of
package or GCL module form.  I'm not sure if there could be advantages
from running ML and lisp based systems in the same memory image.  If
there is interest, someone please so state -- I've downloaded the code
and it almost builds on GCL now.

> 
> > If lisp has a future as well as a past in this field
> 
> My feeling is that its future is really bright.  But as both McCarthy and
> Henry Baker are said to have claimed at the last Lisp meeting, in July,
> standardization (ANSI) is/was bad for Lisp overall.  ANSI, and the AI winter,
> really took the steam out of Lisp.  Bill Schelter, for example, once looked
> bleakly at me when I asked him if he was going to convert AKCL to ANSI, and
> he merely replied, What is the point?  But with good open source ANSI
> compliant Common Lisps now out there, thanks to many, including you, I think
> things are picking up again.  But the next person who proposes to
> "standardize" new extensions to Lisp ought to more seriously consider the
> real costs.  Most importantly, there is Emacs!
> 
> By the way, Gordon Novak once clearly explained to me why the ANSI process is
> so very horrible for software.  The way it works on a big committee is that
> everyone ends up saying I'll vote for your proposal if you'll vote for mine,
> and the result is unintelligibly, incomprehensibly large.  ML had the
> fantastic advantage that Robin Milner had the final say on everything.  There
> is something to be said for benevolent dictatorship, even in software.  But
> not much.
> 

Thanks for the above well taken points.  Wonder what the best way is
to design a language.  I'd just like to see the world's smart people
using the same stuff, which meets their needs optimally or nearly so,
as I believe in the power of unity and synergy.

Take care,

> Bob
> 
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah