[erlang-questions] illegal guard expression: filelib:is_dir(H)

[Richard O'Keefe]

On Feb 16, 2010, at 11:54 PM, Michael Turner wrote:

>
>> He had RUN his program, you see, so he KNEW it was right.
>
> Richard, look, I've run across the same mentality - it was while  
> porting
> some C code, where my boss said it had worked on a couple other
> platforms, so stop foot-dragging, Michael and move on.

Remember, this has nothing to do with formal methods whatever.

I had a student here once who screamed long and loud about the
fact that I had given him 6/10 for a programming assignment.

I said
	Look, the C compiler tells you there is a problem here.
	Using that problem, I can create this one-line legal
	test file that makes your program crash.
	That means your program doesn't work.

He would not, no, I think he honestly COULD not, understand this.
As far as he was concerned,
	The C compiler produces an executable file.
	I don't care what it says along the way.
	The program runs all MY test cases.
	I don't care about yours.
	My program *WORKS* and it can only be deliberate
	malevolence on your part that makes you withhold full marks.

He had RUN his program, you see, so he KNEW it was right,
whatever the C compiler or anyone else's tests or opinions said.

By the way, it's extremely unfair to tar Dijkstra with the
brush of program verification.  He was one of the first people
to say you couldn't expect to write a program and then verify
it.  What he argued for was "deriving the program and its
proof hand-in-hand", which is not an airy-fairy formal methods
idea, but something I've found to be a seriously practical way
to approach hard problems.  The notion of "proof" he had in mind
was very much a human being doing the thinking, not mechanical
verification.  Right now I have a program where I'm having some
trouble, and the whole problem is that I can't show it's right
because I don't have a clear idea of what "right" means.  If I
*did* have a notion of what "right" means, then I could use that
to tell me what to do.

Running a program and hacking on it until it stops being obviously
buggy can be a way of avoiding thought.  If Dijkstra did ever say
what you said someone said he said, then he _might_ for example
have meant that by writing programs in his unimplemented notation
he had resisted the temptation to let hacking serve in place of
understanding what he was doing.

A lot of programming is highly repetitive work, using a stack of
known solutions over and over again.  For that kind of thing,
testing can serve as a defence against typing errors.  *Some*
programming tasks involve solving novel problems, and "rote"
work can be incredibly ineffective for this.  (Dijkstra gave
the example of binary search as a tiny chunk of code that's
much harder to get right than you might think.)

Protocols are one of those things that are incredibly hard to
get right.  (There's a reason why there's a "Dijkstra Prize
in Distributed Programming.")  Reasoning very very carefully
about them using any formal methods and checkers you can get
your hands on pays off, because fixing them by hacking can be
extremely hard.

For a lovely example of how >not< to design protocols, see
http://www.lightbluetouchpaper.org/2010/02/11/chip-and-pin-is-broken/

Does anyone have a good elementary introduction to how to design
protocols between processes?  I know about _testing_ them using
things like SPIN and NuSMV and I'm learning about testing them
using QuickCheck.  But how do you *think* about designing them?
I guess what I'm asking for is "A Discipline of Protocols".

>
> with five other people.  But I knew C and its limits, I knew a bad  
> stack
> crash zone when I saw one, and I can smell bogus assumptions about C
> type sizes and alignments from 50 paces.  That code got fixed.  We
> couldn't ship without it working.  He lost some face over it.
>
> It's not formal correctness VERSUS Real Man Programmers with Grease on
> Their Hands.  I think the problem is that formal correctness got
> oversold on unrealistic merits alone, and after the dashed  
> expectations,
> nobody got in there and sold a practical and credible bill of goods  
> with
> more modest goals.
>
> I mean, look at Peter Deutsch -- his dissertation was about the  
> Stanford
> Pascal Verifier, but he ended up being sort of anti-formalism about
> programming by the mid-1970s, and the exodus continued long after his
> departure.  He loved programming.  The formal correctness people  
> didn't
> give him much to help him love it even more.  Quite the contrary, at
> that point.  So he moved on.  (And his advisor?  I think  
> contributing to
> the SPV with Deutsch was the last thing Richard Karp did in  
> programming
> language semantics.  He had a good nose for where you can get  
> results.)
>
> Things don't happen in the real world until somebody makes the sale.
> And if you screw up the first sale, especially in technology, it can  
> be
> a lo-o-ong time before the idea has a second chance.   The friend of
> mine I quoted earlier sold his boss on the idea of letting him go to
> that Asilomar conference co-starring Edsger Dijkstra by arguing that
> knowledge of formal semantics and tools would help their company be
> competitive.  He came back without any tools to recommend and with a
> dislike of most of what he saw there, especially the attitudes.
>
> I'm sure you're experienced with the phenomenon of something in
> computer science being oversold on unproven merits.  You mention  
> Prolog
> quite a lot, for one thing.  Hey, don't get me wrong, I've got nothing
> against Prolog.  The only reason I'm not elbows-deep into ECLiPSe  
> right
> now is that Erlang soaks up most of the time I have available for
> hacking.  But you know what happened.
>
> -michael
>
>
>
> On 2/16/2010, "Richard O'Keefe" <ok@REDACTED> wrote:
>
>>
>> On Feb 16, 2010, at 2:36 AM, Michael Turner wrote:
>>
>>>
>>>> The reference to Guantanamo is, um, hyperbolic, to put it mildly.
>>>
>>> I plead guilty to Argument by Reference to Wikipedia.
>>>
>>> (A mitigating circumstance: I was once told by a friend that he'd
>>> heard
>>> Dijkstra say, haughtily, at a conference in Asilomar, "'Run a
>>> program'?!  Why, I haven't *run* a program in years!"  Well of  
>>> course
>>> not.  How silly.  Why run programs when you can be proving them
>>> correct
>>> instead?)
>>
>> Let's see, you have a second-hand report of *part* of a conversation,
>> and you base your judgement on that?  What had the other person said
>> to him?  What was the conversation about?  How do you know that the
>> next sentence wasn't "I've often had a computer carry out my plan"
>> or something of the sort?
>>
>> I've just been reading an article in CACM which is simultaneously
>> inspiring and deeply saddening.  The article is about Coverity.
>> The inspiring part is that they've built a wonderful tool for
>> checking C code.  The deeply saddening part is the refusal of many
>> people to believe that their grossly nonstandard code is anything
>> but perfectly legal C.  One example sticks in my mind:
>>
>> 	int a[2], b;
>> 	/* context: sizeof (int) is 4. */
>> 	memset(a, 0, 12);
>>
>> Coverity pointed out the bug.  The customer said "no no, your tool
>> is broken, I *meant* that because a and b are side by side."
>> The fact that the C standard explicitly denies any relationship
>> between the addresses of a and b, and that there have been (and
>> for all I know may still be) compilers that sorted globals,
>> putting the small ones first so it had a fighting chance of
>> being able to address most of them with a single register, which
>> compilers would have guaranteed that a and b were NOT adjacent,
>> all of this was of no importance to the customer.
>>
>> He had RUN his program, you see, so he KNEW it was right.
>>
>> If you want to quote Dijkstra, quote this:
>>
>> 	I would therefore like to posit that computing's
>> 	central challenge, "How not to make a mess of it,"
>> 	has not been met.  On the contrary, most of our
>> 	systems are much more complicated than can be
>> 	considered healthy, and are too messy and chaotic
>> 	to be used in comfort and confidence.  The average
>> 	customer of the computing industry has been served
>> 	so poorly that he expects his system to crash all
>> 	the time, and we witness a massive worldwide
>> 	distribution of bug-ridden software for which we
>> 	should be deeply ashamed.
>> By the way, this doesn't contradict Armstrong's "Let it crash"
>> dictum.  Joe is talking about _components_ hidden inside a
>> system crashing.  Erlang *systems* aren't supposed to crash,
>> which is why Francesco Cesarini and Simon Thompson stress
>> early on in their wonderful book that processes should be
>> watched by some other process.
>>
>> Whether Dijkstra personally ever ran a program or not (and he
>> devised the implementation techniques at the heart of Java),
>> his _notation_ deserves a reasoned responds on its own merits
>> for what it is, not what it might be imagined to be.
>>
>>
>>
>