Re: ADA Popularity Discussion Request

[Jean-Marc Bourguet <jm@bourguet.org>]

jayessay <nospam@foo.com> writes:

> Jean-Marc Bourguet <jm@bourguet.org> writes:
> 
> > jayessay <nospam@foo.com> writes:
> > 
> > > Jean-Marc Bourguet <jm@bourguet.org> writes:
> > > 
> > > > jayessay <nospam@foo.com> writes:
> > > > 
> > > > > Jean-Marc Bourguet <jm@bourguet.org> 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