From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,c406e0c4a6eb74ed X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news1.google.com!news.glorb.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!feed2.news.rcn.net!rcn!feed3.news.rcn.net!not-for-mail Sender: jsa@rigel.goldenthreadtech.com Newsgroups: comp.lang.ada Subject: Re: ADA Popularity Discussion Request References: <49dc98cf.0408110556.18ae7df@posting.google.com> <6F2Yc.848$8d1.621@newsread2.news.pas.earthlink.net> <87eklg62x8.fsf@news.bourguet.org> <878ybnmdzi.fsf@news.bourguet.org> <87y8jmq7x7.fsf@news.bourguet.org> From: jayessay Organization: Tangible Date: 07 Sep 2004 14:29:14 -0400 Message-ID: User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: DXC=5kGkB5Y_Zcjo?iRBY^D> Jean-Marc Bourguet writes: > jayessay writes: > > > Jean-Marc Bourguet writes: > > > > > jayessay writes: > > > > > > > Jean-Marc Bourguet writes: > > > [...] > > > > The problem here is that this application has tried to hack up some > > > > lame version of half of Lisp, > > > > > > The extension language I wrote about was a scheme with > > > some OO extensions and then others. Not a full CL but > > > not something I'd call a "lame version of half of Lisp." > > > > I can't determine this from the above. > > I know that info was not available without doing some hunt > and inference work. But why did you assume that it was lame > and dismissed my points as not related to the issue at hand? > > Do you still think my points are not related to the issue at > hand? Why? The information still suggests that this is indeed a hack on of some subset of a Lisp into the application. What is not clear is whether this was hacked up by the developers of the application or whether they found something (in the public domain or elsewhere) which was some partial hack up which they then included. The former is a classic Greenspuns's tenth, the latter is a variant. > > > > Proving things above the fairly simple level in > > > > software falls victim to the halting problem. > > > > > > Do you really mean what you wrote. If so, I'd suggest > > > you to look a little more to formal proof systems. > > > That's not because the full problem can not be solved > > > that no usefull sub-problem can. > > > > Never said that nothing can be proved. Nor that nothing > > useful can be. > > Reading the quote above, I understood that nothing not > fairly simple can be proved. That's not my experience. > Some quite complex invariants can be proved true with static > type checking. More complex one can be proved by more > powerfull static checker (some of which are able to do type > inference BTW). Yes, formal static typists (in the mold of Hindley and Milner and the type system they independently discovered and which is basically at the heart of any current implementation of a formal type system) can indeed prove some useful even interesting things. What they cannot prove (except in "fairly simple cases") is anything like program correctness. This is largely due to the fact that "correctness" here is a vague concept. /Jon -- 'j' - a n t h o n y at romeo/charley/november com