| Let's define two different kinds of programming: goal-directed and play. (Or
call them what you will.) Play programming is addressing the question "what can
I do with this?" Just like any play, it's useful for learning about whatever
you're playing with.When I was a young programmer, I had a need to express the
contents of a binary tree in lexicographic order. My first solution was several
pages of code (24 cards per page of the coding form we used). I decided to play
with it, since I was not satisfied with the solution – it was ugly. I
tried several more times, learning from each try. The last solution was three
lines, but elegant – nowadays, preorder traversal is standard practice,
but in 1965, the utility of recursion was not readily obvious, and there were no
CS classes to learn it from.
Goal-directed programming is what's usually
practised, at school or at work. The practitioner is given some input (usually
as specifications) and given a goal of creating some output. (My tree traversal
was play, in a goal-directed environment: I had input and a specified output,
but I played with how to do it.)
What a programmer addresses is:
What
have I got?
What should I end up with?
How can I derive what I need
from what I've got?
regardless of his approach, that's his thought patterns,
his analysis. He may go top-down ("how" oriented), front-to-back
(input-oriented), back-to-front (output-oriented), or some other direction or no
direction at all, but he breaks the problem down into smaller problems and
applies the same analysis to each of the smaller problems. The recursion ends
at each branch when the smaller problem is directly soluble in the requisite
programming language, that is, when the smaller problem admits of a solution
synthesis. (Yes, PolR, what is being synthesised is a mathematical construct,
some programming in a mathematical notation [programming language]. We must
never forget that.)
So let's look at "formal programming":
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.
This is a formalization of the programming process:
What have I got? Preconditions.
What should I end up with?
Postconditions.
How can I get from here to there?
Derivation.
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.
In
practice, it's not just "a very powerful way to develop software." It's the way
that goal-directed (and some play) programming is done, in all cases. If you
have done the derivations correctly, the program is as correct as the input and
output specifications.
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%.
Let's correct
that for the general case, applying to all goal-directed programming: "For
anything more than a trivial project, the likelihood of errors in the
proof derivation approaches 100%." Thus we have Windows, Java,
Flash, and all the myriad of other programming errors in the wild.
The basis
of "formal programming" is the application of sound (formal) methods of analysis
and synthesis to goal-directed programming — nothing more, nothing less.
This is propounded as a substitute for the informal, error-prone methods most
often used.
I prefer to look at the more productive result: when a
programmer is knowledgeable about the formal basis of his methods, he is better
able to use the informal methods in a formal and correct fashion, thereby to
greatly reduce the errors in his work. That's the way I've used the formal
methods, anyway. It's not very different from arithmetic: the more you
understand the formal bases for number fiddling, the better you can become at
it. ---
--Bill. NAL: question the answers, especially mine. [ Reply to This | Parent | # ]
|
