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!news2.google.com!proxad.net!feeder2-1.proxad.net!news11-e.free.fr!not-for-mail 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> From: Jean-Marc Bourguet Date: 07 Sep 2004 19:56:52 +0200 Message-ID: <87y8jmq7x7.fsf@news.bourguet.org> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Organization: Guest of ProXad - France NNTP-Posting-Date: 07 Sep 2004 19:56:20 MEST NNTP-Posting-Host: 82.253.214.171 X-Trace: 1094579780 news11-e.free.fr 9272 82.253.214.171:32773 X-Complaints-To: abuse@proxad.net Xref: g2news1.google.com comp.lang.ada:3444 Date: 2004-09-07T19:56:20+02:00 List-Id: 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? > > > 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). Yours, -- Jean-Marc