Re: Patterns and Compositionality

> I didn't say it was impossible -- I said that it's not easy.
I didn't say it was easy with lambda-like formal calculi.
I said it was as easy/difficult with such calculi as with any formal calculi,
including sequent calculi that you like.

> proofs involving the resulting messes are a nightmare.
Not any _more_ than with any calculus for imperative programming.
Imperative programming IS a nightmare, stop.
Using an imperative calculus as a "primitive" calculus
is an abstraction inversion.

> Nonsense!  Computers and even turing machines handle those _easily_.
Not easily. The semantics of computers and turing machines is quite contorted.

>> Friends have done proofs of imperative programs (heap 
>> sorting, and more)
>> in Coq (a logic system based on pure typed lambda-calculus); 
>> it's possible,
>> but it's certainly not straightforward.
>
> Have you seen the proofs on similar systems written using abstract state
> machines?  The proofs are readable by anyone with a reasonable amount of
> perseverence.
>
So are proof sketches in frameworks such as the one used by Coq.
The part that's not straightforward is going from the proof sketch
to the precise, machine-checkable proof. Having worked with proof checkers
for an imperative framework (B, a dialect of Z), I can tell that the latter
is certainly not simpler.


> Fare', you're too hung up on formality.  Not everything has a formal
> definition!
Not everything. But everything that can be usefully used
for technical collaboration over e-mail.

> "Design Patterns" are like "sewing patterns". Opposing them is
> like opposing sewing patterns because they're only shapes, and geometricians
> have known about shapes all along.
In as much as there is a meaning in "Design Patterns", I do not oppose them
(see below). What I oppose is the very approach of hyping around
"Design Patterns", and presenting it as something that's new and the be all
end all of programming methodology, whereas it's plain old and has been
the very basis of programming since the very beginning (long known as
"pseudo-code"). Similarly, just because I oppose "OO",
"programming by contract", "<FOO> Methodology", "Java",
and the rest of the industrial hype doesn't mean that I reject
the good things about them (that none of them brought about,
but instead borrowed from better previous works).


> A realistic definition of a "pattern" in that sense is "how it's been done
> before".  Perhaps the words "role model" serve better.
No. A realistic definition of a "pattern" is meta-information
(that you can alternatively consider as snippets of metaprograms
for an arbitrarily declarative language).
Yes, meta-information is useful. But just giving it a brand new name
and hyping around informally instead of building formal tools to take
advantage of it, is not progress but a brake to progress.


>>>  Hype is the entire basis of our devotion to Tunes,
>>>  and Fare is responsible for that.
>>>  So hype can be used for good as well as evil ;-).
>
>> No comment.
> It's one of the more important things I said.
>
> Patterns are useful and expedient.  TUNES is also useful, but not always
> expedient.  Hype claims to be useful, but is never expedient.  TUNES is
> closer to hype than patterns are.
>
Meta-comment: I am convinced that Tunes is not hype,
but I admit I haven't given a proof of it yet;
thus I reserve a comment for later (when I am no more convinced,
of have given a suitable proof). And yes, I'm responsible for all
of Tunes' shortcomings.

Regards,

[ François-René ÐVB Rideau | Reflection&Cybernethics | http://fare.tunes.org ]
[  TUNES project for a Free Reflective Computing System  | http://tunes.org  ]
How do you know that what you call ``blue'' is the same as what someone else
calls ``blue''? What if someone else's feelings for red and blue are
interverted as compared to yours? These questions are irrelevant, because
the meaning of things doesn't lie in an unobservable intrinsic nature,
but precisely in their observable external behavior. There is no achievable
objectivity beyond the union of all possible intersubjectivities.
                -- Faré