Re: Response to Karen and to Willem on recursive proofs

From: Edward G. Nilges (spinoza1111_at_yahoo.com)
Date: 02/02/04 

Date: 1 Feb 2004 20:38:43 -0800

Ian Woods <newspub2@wuggyNOCAPS.org> wrote in message news:<Xns9482814D24B24newspubwuggyorg@217.32.252.50>...
> spinoza1111@yahoo.com (Edward G. Nilges) wrote in
> news:f5dda427.0401312028.447bfd18@posting.google.com:
>
> > blmblm@myrealbox.com wrote in message
> > news:<bvdfqm$r3s5l$1@ID-147531.news.uni-berlin.de>...
> >> In article <f5dda427.0401281831.dade6d9@posting.google.com>,
> >> Edward G. Nilges <spinoza1111@yahoo.com> wrote:
> >>
> >> [ big big snip ]
> >>
> >> [ this was me in an earlier post ]
> >> >> > But it is a little disturbing to consider the implications of
> >> >> > the fact that the proofs take place in a universe with integers
> >> >> > and real numbers, while the programs run in a universe with ints
> >> >> > and doubles/floats, which don't quite have the same properties.
> >> >>
> >> >> s/the proofs/some invalid proofs/
> >> >
> >> >No, the guy's point is well taken. You cannot deductively "prove"
> >> >that some clown won't misuse your code.
> >>
> >> If I am the "guy" to whom you refer (where I assume you mean "guy"
> >> as a gender-neutral term), I'm not sure how your comment relates to
> >> what I said. Even if your factorial function came with a disclaimer
> >> that it would only work for inputs N such that N! can be represented
> >> as an int, the proof doesn't look at that aspect, does it? Such
> >> proofs usually don't. That was my point.
> >
> > OK, I understand that int precision controls the absolute validity of
> > the proof. But as hero computer scientist Edsger Dijkstra has
> > pointed-out, programming is APPLIED mathematics.
>
> So why post an invalid proof as an attempt to prove something? Clearly,

Because programming is APPLIED mathematics.

My physics teacher warned us that in the everyday lab, we should not
credit measurements, made with actual, ordinary equipment, to more
than two places of precision. But this did not entail, for him, that
measurements made to this precision were invalid, which seems to be
your contention.

Hero computer scientist Dan McCracken, in Numerical Recipes and
Fortran Programming, was one of the few Fortran writers to warn
programmers about being misled by Fortran's excess precision, because
these early giants had the humility to realize that they are applied
mathematicians.

It appears that computer scientists with heroic exceptions like
Dijkstra and McCracken actually believe that they are pure
mathematicians. They have in this replaced the original joy of
creation, in actual (applied) programming with its anhedonic and
bipolar reverse lest someone upset their ricebowl, in part by foul
disrespect of simple praxis and foul disrespect of its necessary link
with theory.

Dijkstra, in March of 1968, actually invented a technique which
ordinary programmers could use, and when Dijkstra turned his attention
to operating systems, he repeated this accomplishment, for which he
deserved the equivalent of a Nobel prize. This burned the ass of
lesser men in his day and as a result Dijkstra's memory is being
apparently erased.

But having being corrupted by "maturity" (that is, access to money and
power), it now becomes the tasks of academics to instead control the
supply of that information, that wants to be free. This task is
carried out by labeling and using third hand sources to write the
biography of others in an insulting fashion.

> if the proof isn't based on the mathematical behaviour of the axioms from
> which the code is derived then it's not valid. The valid set of values
> for specific types are part of those axioms. If the proof does not
> include these definitions of fundamental code behaviour you've not proved
> anything about the code.

Depends on what you mean by proof, Ian.

I sense that Euclid's concern was equally establishing timeless truths
about lines in the sand, AND communicating a memory of those truths
independent of the vagaries of the sand. But this seems to be
forgotten by modern pure mathematicians, and compsci types who are
such unconscious Platonists that they do not realize that they are the
hired hands of money and power, until their job goes to India, where
sufficient social solidarity means that work gets done.

To me, a proof is necessarily a teaching, even a self-teaching device.
Indeed, that's why I found Willem's proof illuminating...despite the
fact that it's subject to the same precision critique as is mine, a
fact that's being conveniently ignored by the trolls' chorus, which
you have joined against the better angels of your nature.

>
> > This is paradoxical, since Dijkstra had when alive such a reputation
> > as a theorist's theorist, and was so often dismissed (by people like
> > Yourdon who cashed-in on his ideas) as ivory tower.
> >
> > What it means of course is that any proof is "bounded" by its
> > application. No civil engineer asks of the mathematics of
> > bridge-building that it foresee the physical conditions that actually
> > apply, nor do civil engineers reject math because of this limitation.
>
> Do we expect mathematics to foresee? No, that's the engineers job. Model?
> Yes. If when building bridges you decide to pretend it's spanning a
> crater on the Moon instead of over a river on the Earth you're not going
> to have a very good bridge. If you're going to use mathematics to prove
> something (that the code operates as specified, that the bridge operates
> as specified) you model as precisely as sensible. In computing, most of
> the universe is axiomatic and hence there is no excuse not to model it
> correctly.
>
This is false. If hero computer scientist Dijkstra is right, then as
applied math, compsci's universe includes the social world.

This is difficult for a generation of compsci types into whom
antipolitics has been beaten by Thatcher and Reagan, but part of the
80% failure rate of enterprise systems results from denial, and a
forced agreement with the mad woman Margaret Thatcher's "there is no
such thing as society".

To sniff like a maiden aunt, "there is no excuse" is to be in denial
of the reality of computing, for we can open up even "axiomatic" texts
like Numerical Recipes and find unacknowledged stylistic bugs, such as
the idiotic use of a font in which 1 and I are nearly indistinct.

To sniff like a maiden aunt, "there is no excuse" is to ignore that in
supercomputing, Fortran persists and so does the preservation of
Fortran-style errors. If there is no excuse, then why have no funds
been made available for a complete rewrite of large, mission-critical
systems in Ada? My suspicion is that the social mechanism that
followed Bush's idiotic speech about Mars, with the promise to destroy
the Hubble telescope, applies, and its name is the reversal of
enlightenment in the service of money and power.

To sniff like a maiden aunt, "there is no excuse" is to equivocate
over a fissure in computing considered as a social reality. This is
the socioeconomic divide between the elite, which presents the idea of
a computing system as independent of society and history, and indeed
as "axiomatic", and the operationals who must then construct the
non-Platonic reality.

Unless they were to use a RISC machine with unbounded precision
implemented in software, that has access to unbounded virtual memory,
the "mere coders" must use, in the case of numeric precision, a fixed
number of bits per real or integer, and for this reason, ANY axiomatic
proof of their code is similar to a laboratory measurement that is
bounded by common goddamn sense.

You have, like all the members of the troll's chorus, irresponsibly
used third-hand impressions of an argument made, and you have labeled
the application of proof techniques to real code as a "Nilges"
technical foul...despite the fact that applying what Willem knows to
real code is both a teaching and an understanding device!

My conclusion is that academic compsci is now corrupt by a false
promise, that owing to the prestige, the money, and the power,
academic computer scientists may be, like pure scientists, considered
as Platonic temple priestesses and indeed, now, guardians of the
secrets of this particular temple of doom...so that the mere unwashed
do not use them as of old.

To sniff like a maiden aunt, "there is no excuse" is to ignore the
fact that September 11 may have been in many ways a confirmation of
hero computer scientist Dijkstra's dark prediction that industrial and
social organizations may well collapse under the weight of unmastered
complexity. FBI agent Colleen Rowley testified before Congress that
she did not even have buggy Boolean evaluation in the FBI data base,
and, post September 11, our precious Administration is reduced to
speaking darkly of levels of mere stochastic noise as credible threat
levels and as excuses for violations of the Constitution.

Colleen might have, as users have over time, welcomed a Boolean
evaluation tool that ran slowly IF she entered queries, let us say,
longer than 255 characters owing to the use of strlen in for, or one
with bugs she could workaround.

This isn't to defend poor practice or bugs, although I am certain it
shall be re-presented in that way by the Troll's Chorus. It is only to
say that computing is an applied and not a pure science.

It's dollars to donuts that Platonism within MIS at the FBI shitcanned
any simple addition of Boolean queries, for the Platonism of
non-coders causes them to yearn for something not made of code by
programmERs. This newsgroup, Richard tells us, has nothing to do with
humanity, and the merely human is shown the door.

Our leaders of "homeland security" speak of stochastic noise because
although there is "no excuse" in your twittering axiomatic world,
somehow they don't have the tools to Constitutionally defend against
threats, or avoid angering poor men by lazily letting Israeli and
Pakistani thugs do their dirty work.

This is because compsci types, being apolitical, are very good at
creating operating systems without even getting paid, but no good at
all in seeing to it that real systems meet the needs of stakeholders,
contextualized in society.

Instead they create systems by means of which they themselves are
deprived of retirement as at IBM and which allowed Enron to fabricate
companies at warp speed.

Like it or not, I use recursion, for example to design test data for
zero records, one record, and n+1 record. And in an on-topic manner I
have narrated this experience on this newsgroup only to find that
what's ontopic is negativity and foul disrespect.

My next stunt in fact shall be to post a free regular expression
explainer and I shall be amused by the resulting brou ha ha.
 
> <snip the rest>
>
> Ian Woods

Loading