Re: [tlug] [OT] Good IT Resume

["Stephen J. Turnbull" <stephen@example.com>]

Curt Sampson writes:

 > Surely if, without overspecifying, one can come up with a picture or an
 > English prose description of something designed to be implemented, one
 > can also, with some further work,

I thought you were opposed to such makework. ;-)

 > come up with a more formal description that would be more amenable
 > to a formal proof of correctness and interpetable by a computer,
 > both of which are indisputably Good Things.

C'mon, man, I'm a social scientist, you can't fool me with that
nonsense.  Both of those are good things, but in general irrelevant to
the specification problem, which is the problem of tying human wants
to physical reality.

In other words, a specification is something that the customer can
understand.

Formal languages are cool for this kind of thing:

Boss to security expert: I want a secure system.
Security expert to engineer: I want a provably secure system.
Engineer to security expert: Here's the Z code, the proof, and the
    test runs.
Security expert to boss: It's OK, trust me.
Boss to security expert: [thrusts elbow against Adam's apple of
    security expert] Good, I trust you, and I also know where you
    live.  Still OK?
Security expert: [chokes] Y-y-y-esss.

But take out the fully-trusted security expert, and you're going to
have to talk to the boss in English prose; he will not sign off on Z
code that he doesn't understand (or if he does, it's time to get your
resume in order).

As I already mentioned, in combination with short glosses about what
aspects of an implementation are specification and what parts are
incidental, code is often used to specify protocols.  Other formal
notations, such as BNF, are rampant in RFCs.  *But* eventually you
have to tie things to humans.

Eg, on the Mailman-Developers list we're discussing a spec for archive
URLs so that (eg) a person who was CC'd and did *not* get the mail
from the list can find the thread using only public information (the
archive's base URL) and a relative URL computed from the message
headers.  There is a required relative URL (based on the message ID)
and there is an optional globally unique relative URL, which might not
necessarily be implemented by mirrors.  Now, what HTTP error should be
returned if retrieval via the unique URL is not implemented?  The two
that came up were 501 UNIMPLEMENTED and 410 GONE, but it was only
after reading the prose specs for those, including use-case examples,
that it became clear that 410 is wrong and 501 is the appropriate
answer.

I really don't see how a Z-code spec can help with such issues.