!Owen -
I can't wait for Marilyn Monroe (with a Groucho Marx moustache and cigar
and Nick Thompson eyebrows) to break into "Happy Birthday Mr. Computer
Guy!, Happy Birthday to you.... "
I have to say (Owen) that this doesn't even come close to any reality I
live in:
"The general problem os software verification is not solvable by
computer". (sic)
This would never work at any cocktail party I've been to... I admit it
might be the simplest way of saying it that has a chance of being
explained in *one more* unpacking, but is more likely to just end the
conversation (young lady with Nick's eyebrows cocks her head and says "I
think I hear my stock broker calling!" as she walks off). So maybe your
approach to progressive disclosure is more "recursive" than "iterative".
If her "Big Bold Naivete" comes with her "Nick Thompson eyebrows", she
might stick around for another couple of rounds of unpacking. Like
"what in heaven's name does 'software verification' have to do with
anything, and why would I *care* if you can do it with a computer or not?".
In facte I would claim that *almost literally* anyone who understands
your postulation:
"The general problem os software verification is not solvable by
computer".
agrees with it, and anyone who doesn't probably has *virtually* no clue
what you are talking about?
I admit that Nick (in Marilyn drag) has set you up a little by using
words like HALTING, suggesting the (s)he has a more familiar
vocabulary/lexicon than in fact (s)he probably does. I suppose anyone
who knows the technical definition of "halting" probably already
understands the phrase:
"The general problem os software verification is not solvable by
computer".
Beyond this, I don't understand why someone (Owen?) would understand
this phrase:
"The general problem os software verification is not solvable by
computer". (sic)
yet would imagine that the rigorous methods of computer science would
put Philosophical questions to bed. I'd suggest that *most* of
Philosophy has been hand-verifying programs written in logic,
classifying them, and creating an (ever growing?) bin of "quite possibly
undecidable" (but non-trivial and interesting) statements. I sense
that you (Owen) don't agree/believe that this ever-growing bin is a
*result* of the application of very formal methods (although driven by
intuition and executed in psuedo-natural language) rather than *in spite
of* the same?
- Steve
"But Mr. Densmore: what is the problem of software verification."
I would bat my eyes, by my eyebrows would get in the way.
Nick
*From:*Friam [mailto:friam-boun...@redfish.com] *On Behalf Of *Owen
Densmore
*Sent:* Wednesday, April 17, 2013 3:03 PM
*To:* The Friday Morning Applied Complexity Coffee Group
*Cc:* Frank Wimberly
*Subject:* Re: [FRIAM] Isomorphism between computation and philosophy
On Wed, Apr 17, 2013 at 10:27 AM, Nicholas Thompson
<nickthomp...@earthlink.net <mailto:nickthomp...@earthlink.net>> wrote:
<snip>
So, Owen, you meet a beautiful woman at a cocktail party. She
seems intelligent, not a person to be fobbed off, but has no
experience with either Maths or Computer Science. She looks deep
into your eyes, and asks "And what, Mr. Densmore, is the halting
problem?" You find yourself torn between two impulses. One is to
use the language that would give you credibility in the world of
your mentors and colleagues. But you realize that that language
is going to be of absolutely no use to her, however ever much it
might make you feel authoritative to use it. She expects an
answer. Yet you hesitate. What language do you use?
Your basic English.
You would start, would you not, with the idea of a "problem." A
problem is some sort of difficulty that needs to be surmounted.
There is a goal and something that thwarts that goal. What are
these elements in the halting PROBLEM? And why is HALTING a
problem?
Well, I do get asked a lot about computation and have found a
"progressive disclosure" approach best. I'd start by saying exactly
what Michael Sipser, Intro to Theory of Computation, does:
"The general problem os software verification is not solvable by
computer".
Usually that is clear enough but if more is needed, we progressively
discuss what software is and how it is modeled in computer theory.
Believe it or not, I've had this sort of thing lead to Finite State
Automata, first as circles and arrows but then to the formal 5-tuple.
And this was not a mathematically sophisticated person.
-- Owen
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
