Re: ADA Popularity Discussion Request

[jayessay <nospam@foo.com>]

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:
> > > > 
> > > > > 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.

Presumably you mean Elisp.  No it is not, it is just a well known
_broken_ Lisp.


> 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.

You are making a change to the preconditions so that the new ones are
no longer a subclass of the former.  Therefore all callers will need
to be checked.  Note, the preconditions (the new or the original) may
not even be definable in terms of any type system.


> 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.

Or big extremely slow compiles which may not catch this either.  This
sort of problem is beyond language issues (see Ariane 5...)


> > 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.

Exactly - and off you go down the rabbit hole.

>  At time it can be more conveniant but currently it looks to me like
> more a niche thing.

I agree.


> 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.

I think this is largely due to the fact that these things pretty much
require 1) no side effects 2) no procedural descriptions.  The real
world (tm) OTOH, is largely made up of things that have both of
these...


> You can use type system to state and verify invariants.  And that's
> something available now.  And it is usefull.

No one said it wasn't.  I merely claim that dynamic system can do this
and more.  Obviously you don't believe me.  That's OK.


/Jon

-- 
'j' - a n t h o n y at romeo/charley/november com