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