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!news2.google.com!proxad.net!feeder2-1.proxad.net!news13-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> <87y8jmq7x7.fsf@news.bourguet.org> From: Jean-Marc Bourguet Date: 07 Sep 2004 21:03:55 +0200 Message-ID: <87ekldrjdw.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 21:03:23 MEST NNTP-Posting-Host: 82.253.214.171 X-Trace: 1094583803 news13-e.free.fr 28452 82.253.214.171:32784 X-Complaints-To: abuse@proxad.net Xref: g2news1.google.com comp.lang.ada:3447 Date: 2004-09-07T21:03:23+02:00 List-Id: jayessay writes: > 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. Do you think emacs is a case of case of Greenspuns's tenth? The program I'm speaking about is very similar to emacs in architecture. But the problems I was speaking about could also occur in any program in CL of comparable size and complexity. Modify some middle or low level function and break one of its user which didn't respect one of its pre-condition in a way which was harmless with the previous implementation. Where is the problem? In the new code? It respect the documented interface. And testing can only show the problem in big, slow integration tests. In the client code? Well no testing could show the problem when it was written. > > > > > 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. Agreed, program correctness is too vague. You can try to find equivalence with a formal description, but then you have to proove that that description is correct. At time it can be more conveniant but currently it looks to me like more a niche thing. Most of the bugs I've to track are due to breaking invariants. Especially thoose stated no where invariant or with a formulation no more in sync with the code. Those formal systems can proove invariants and using them to do so would be usefull. But I know of no mainstream system with that available. You can use type system to state and verify invariants. And that's something available now. And it is usefull. Yours, -- Jean-Marc