🚀 go-pugleaf

Michael Coffin >
Me             >|

>|eh?  imperative programming languages don't say "achieve this goal" ?
>No.  Imperative languages specify a series of actions, not the
>results of those actions.

umm.. hmm...

I'm not totally sure I see the difference.

If I have a routine that sorts numbers so that the result is
monotonically increasing, doesn't the closure of that routine with
some numeric list specify the results?

>|...if I say "sort this list" that's [what] an imperative language
>|does.  That's an equivalent statement to "make this list sorted".
>But neither is equivalent to "this list IS sorted", which is what
>proofs allow you to say, and which is the way the specification of
>the sorting program is probably phrased.  The closest you can get in
>an imperative language is saying "Check whether the list is sorted;
>if it isn't, abort the program or raise an exception".

Er.. yes, in that proofs generally are sets of equivalent statements
about the same "data" (often denumerable sets, or what-have-you).  But
even in proofs, you can deal with expressing A in form B.

But if I have a routine called "sort" which sorts, and I feed a list
into it which it can sort, the result is a sorted list.  Somebody has
to establish that "sort" does indeed sort, but that would be true of a
formal proof as well (you need to establish that you have a definition
of "sorted" which fits within your formalism -- or else accept a
priori that there is this thing called "sorted" and use its
properties).

I'll grant you that an imperative language transforming data is doing
something different than a proof about some form(s) of that data.  But
what about an imperative language transforming some set of statements
to some equivalent set of statements (like a compiler, or a symbolic
math engine)?

I think it's just a matter of what's being transformed.

No??

Well, I guess some proof techniques are O(godawful).  But that's what
people are for...

>Encapsulating in a procedure named "sort" all the swaps that
>accomplish sorting just pushes the problem down a level.  The
>question remains: how do I know that after calling "sort(x)" the
>array x is sorted?  Well, I can either test the routine "sort", or I
>can prove that after calling it the array will be sorted.

Hmm... so what you're talking about is introducing new concepts to a
language or system.  I think that technically this falls into the
category of "meta-proofs" rather than "formal proofs".

Correct me if I'm wrong :-)

I know somebody will...

Raul Rockwell