|
|
|
| Authored by: emmenjay on Wednesday, September 05 2012 @ 12:32 PM EDT |
Hi Bill
I have read the two Dijkstra papers you mentioned. (My progress has been
glacial as my health has not been good).
On the second paper: "EWD498: How do we tell truths that might hurt?",
I won't comment much. It sounds like a programmer bemoaning the current (at
that time) state of the art in programming tools. Much of what he says is
reasonable, but I'm not certain where it fits in our discussion. If I've missed
something important (quite likely) please enlighten me.
The first paper: "EWD 924: On a cultural gap" is interesting, but
possibly less relevant than it might have been.
If I'm understanding correctly, Dr Dijkstra is referring to a technique called
"Formal Programming". This is a fascinating technique but its impact
on modern software developemnt still remains fairly small. See also David
Gries, "The Science of Programming", Springer, 1981.
To grossly oversimplify, formal programming goes roughly as follows:
-- Describe a set of "preconditions" -- the state at the start of
program execution.
-- Describe a set of "postconditions" -- the desired state at the end
of program execution.
-- Mathematically derive the logic to go from pre to post.
Now in theory, this is a very powerful way to develop software. After you
finish the software you have great confidence in its correctness, which has been
proven by the development process.
However formal programming never really caught on, except for a few small areas.
One of the main problems is the complexity of the proofs. For anything more
than a trivial project, the likelihood of errors in the proof approaches 100%.
The cure for this was seen to be automating the proof process. Some interesting
work was done on this by Prof. Ken Robinson et. al. at Uni of NSW (Australia) in
the late '80s, but I lost contact with that group and don't recall seeing
anything come of the work. A couple of years ago, I met a post-doc student at
UNSW who told me that the automation was just about complete and was working
reliably. I expect that we may see formal programming make a comeback on the
strength of that, but so far I haven't seen anything.
So I perceive that Dr Dijkstra is referring to how he things software ought to
be, rather than how it is.
While I have a little experience in this are, I am far from an expert. If I
have it mixed up, please explain it to me.
Regards
Michael J Smith. [ Reply to This | Parent | # ]
|
|
|
|
|
