Is program proving viable and useful?
Is program proving a viable and useful endeavor? Does it create more problems than it solves?
Today I participated in a reddit discussion thread. The discussion brought up some issues I care about, and I think others will care also.
Although I’m quoting from another person whose viewpoint may contrast with mine, I mean no insult or disrespect to him. I think his views are fairly common, and I appreciate his putting them into writing and stimulating me to put some of mine into writing as well.
[…] you could specify the behavior it should have precisely. However in this case (and in most practical cases that aren’t tricky algorithms actually) the mathematical spec is not much shorter than the implementation. So meeting the spec does not help, the spec is just as likely to be wrong/incomplete as the implementation. With wrong/incomplete I mean that even if you meet the spec you don’t attain your goal.
I like the observation that precise specifications can be as complex and difficult to get correct as precise programs.
And indeed specification complexity is problematic.
Rather than give up on precision, my own interest is in finding simpler and clearer ways to think about things so that specifications can be quite simple.
Thus my focus on simple and precise semantic models.
One example is as given in Push-pull functional reactive programming.
I’m proud of the simplicity of this specification and of how clearly it shows what parts of the model could use improving.
(The Event type doesn’t follow the type class morphism principle, and indeed has difficulty in practice.)
And since such semantics-based software design methods are still in their infancy, I agree that it’s usually more practical to abandon preciseness in software development.
For more examples of formally simple specifications, see the papers Denotational design with type class morphisms and Beautiful differentiation.
I suspect the crux of the issue here is that combining precision and simplicity is very difficult — whether for specifications or programs (or for many other other human endeavors).
Any intelligent fool can make things bigger and more complex … it takes a touch of genius — and a lot of courage — to move in the opposite direction. – Albert Einstein
We had been writing informal/imprecise “programs” for a long time before computers were invented, as various kinds of instructions/recipies. With mechanization of program handling in the 1940s came the requirement of precision. Since simple precision is difficult (according to my hypothesis), and precision is required, simplicity usually loses out. So our history of executably-precise programs is populated mostly by complexity.
I conclude that there are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is make it so complicated that there are no obvious deficiencies. The first method is far more difficult. – C.A.R. Hoare, The Emperor’s Old Clothes, Turing Award lecture, 1980
As much as one assumes that the future is bound to perpetuate the past, one might believe that we will never escape complexity. In my own creative process, I like to distinguish between the notion of necessarily true and merely historically true. I understand progress itself to be about this distinction — the overturning of the historically true that turns out (often surprisingly) not to be necessarily true.
What about specification? Are precise specifications necessarily complex, or merely historically complex? (I.e., must we sit by while the future repeats the complexity of the past?) This question I see as even more unexplored than the same question for programs, because we have not been required to work with formal specifications nearly as much as with formal programs. Even so, some people have chosen to work on precise specification and so some progress has been made in improving their simplicity, and I’m optimistic about the future. Optimistic enough to devote some of my life energy to the search.
Simplicity is the most difficult thing to secure in this world; it is the last limit of experience and the last effort of genius. – George Sand
Everything is vague to a degree you do not realize till you have tried to make it precise. – Bertrand Russell
I expect that future software developers will look back on our era as barbaric, the way we look at some of the medical practices of the past. Of course, we’re doing the best we know how, just as past medical practitioners were.
I know people are apt to hear criticism/insult whether present or not, and I hope that these words of mine are not heard as such. I appreciate both the current practitioners, doing their best with tools at hand, and the pioneer, groping toward the methods of the future. Personally, I play both roles, and I’m guessing you do as well, perhaps differing only in balance. I urge us all to appreciate and respect each other more as we muddle on.
Charles23:
What is the difficulty in practice with Event?
3 January 2010, 4:10 pmconal:
@Charles: A monad associativity law can fail in some cases. Thanks, QuickCheck! It’s been quite difficult to chase some subtle strictness problems out of the implementation. I hear
3 January 2010, 7:36 pmunambworks better in GHC 6.12.1, so there may be some progress, but I’m still wary.Jeff:
I think the real value of formal methods aren’t in formalizing vague specifications of what the code is supposed to do at a high level. Of course you can’t formalize “help me track my budget” or “entertain me with a fun game” or “browse the internet”.
What you can formalize is the stuff that the programmer knows the code should be doing, but can’t currently express at compile time. This function should return a list sorted by account ID. That function requires a list sorted by account ID to work correctly. No two of these game objects should ever be assigned the same grid position. This function is guaranteed to return one of these known document types no matter what input stream it is given. That function will always return in some bounded time, using a known set of resources.
In other words, you can’t prove everything, but there are still huge gains to be made proving more than we do today.
My hope is that such proofs will look exactly like quickcheck tests, and quickcheck will someday turn into a tool that proves what it can, and for the rest says, “I couldn’t prove it, but at least it passed these test cases.”
4 January 2010, 2:39 pmNorman Ramsey:
Conal,
Nice blog. From my perspective as a teacher, I find that one of the most difficult lessons to teach is that complexity is the enemy. Many young people enjoy complexity—perhaps it gives them a feeling of mastery or something. And as you’ve pointed out, simple and precise is much harder.
In more than just programming, this is not an age given to the appreciation of simplicity.
Norman
4 January 2010, 6:57 pmmuad:
Hi Conal, I don’t understand this post. what do you mean?
7 January 2010, 2:13 amLinktipps Februar 2010 :: Blackflash:
<
p>[…] das eine Frage sein, die sich heutzutage er
14 January 2010, 9:16 amjfoutz:
@muad
There are good abstractions out there waiting to be found. Just because the specification we have now is bad/good/whatever, that dosn’t mean there aren’t better abstractions just waiting to be found.
26 January 2010, 12:05 pmconal:
@jfoutz: Yeah — you got the message. Thanks for the paraphrase.
We have been forced to make our programs precise, but we haven’t been forced nearly as much to make our specifications precise. So there’s been more progress on simple precise programs than on simple precise specifications. Without noting this historical difference, one might mistakenly assume that precise specifications are inherently resistant to simplicity.
26 January 2010, 6:13 pmthomash:
Both programming and specifications have a common requirement: abstraction. So maybe working on precise programs was not all lost on specifications, as we “trained the right muscles”, so to speak. There is a bit of lore concerning complexity in the programming realm, and personally I like to think that reducing complexity is the crown jewel of all the activities involved with programming. What many people miss, though, is that it is often a function of time and effort. A professor once said to us, when we were really young students and faced with our first major assignment, “When you start making your way into your topic, you will find that more and more aspects come up, and you are retrieving more and more books from the library (we were using books at that time!). Don’t be overwhelmed! As you continue your way, you will find that pieces fall into place, and relations are found, and many things turn out to be duplicates or variants of one another, so in the end the amount of material you have to deal with is quite manageable”. Likewise, complexity often has a ballistic curve. Initially, it increases, and people often stop when a program, or a spec, meets the functional requirements, when complexity is usually at its max. Only when you continue you will find that, while still meeting the requirements, the comlexity goes down again. Unfortunately, many system never reach that state.
22 April 2010, 8:29 amconal:
thomash,
Wow — I love this comment! I especially enjoy your description of plowing through complexity, riding the curve up and then down. And I relate deeply. My aim rarely is to get some software merely working (so that it “meets the functional requirements”), but to continue until implementation is compelling, revealing, and ideally inevitable. A tremendously satisfying experience. And a journey of faith, in the sense of hopefulness and willingness to try, but with no guarantee or certainty of outcome. And when it works out, I’m grateful for being invited along for the ride.
And yes (!) to your perspective that in spite of focusing on programs (answers), we will have still “trained the right muscles” for mastering the complexity of specifications (questions).
22 April 2010, 7:51 pmconal:
In the initial stage (extreme ignorance), it’s easy to give up, and confidently claim something cannot be done. When I probe, usually I find that these confident claims are supported only by what I’ve come to call “proof by lack of imagination”. Progress perhaps depends on faith, persistence, even naïvité.
“Ignorance more frequently begets confidence than does knowledge: it is those who know little, and not those who know much, who so positively assert that this or that problem will never be solved by science.” – Charles Darwin
“Dare to be naive.” – R. Buckminster Fuller
“It is our duty as human beings to proceed as though the limits of our capabilities do not exist.” – Teilhard de Chardin
“Things are only impossible until they’re not.” – Jean-Luc Picard
16 January 2011, 5:56 pm