a defense of ad hoc software development
in [Lisp]
|
Prev: Some help with sort
Next: SBCL optimization
From: Mark Tarver on 16 Feb 2010 15:50 On 14 Jan, 14:46, ccc31807 <carte...(a)gmail.com> wrote: > On page 229 of Paul Graham's 'ANSI Common Lisp' he writes: > > <quote> > If programming were an entirely mechanical process -- a matter of > simply translating specifications into code -- it would be reasonable > to do everything in a single step. But programming is never like that. > No matter how precise the specifications, programming always involves > a certain amount of exploration -- usually a lot more than anyone had > anticipated. > It might seem that if the specifications wee good, programming > would simply be a matter of translating them into code. This is a > widespread misconception. Programming necessarily involves > exploration, because specifications are necessarily vague. If they > weren't vague, they wouldn't be specifications. > In other fields, it may be desirable for specifications to be as > precise as possible. If you're asking for a piece of metal to be cut > into a certain shape, it's probably best to say exactly what you want. > But this rule does not extend to software, because programs and > specifications are made out of the same thing: text. You can't write > specifications that say exactly what you want. If the specification > were that precise, then they would be the program. > </quote> > > In a footnote, Graham writes: > > <quote> > The difference between specifications and programs is a > difference in degree, not a difference in kind. Once we realize this, > it seems strange to require that one write specifications for a > program before beginning to implement it. If the program has to be > written in a low-level language, then it would be reasonable to > require that it be described in high-level terms first. But as the > programming language becomes more abstract, the need for > specifications begins to evaporate. Or rather, the implementation and > the specifications can become the same thing. > If the high-level language is going to be re-implemented in a > lower-level language, it starts to look even more like specifications. > What Section 13l.7 is saying, in other words, is that the > specifications for C programs could be written in Lisp. > </quote> > > In my SwE classes, we spent a lot of time looking at process and > processes, including MIL STD 498 and IEEE Std 830-1984, etc. My > professors were both ex-military, one who spent his career in the USAF > developing software and writing Ada, and both were firmly in the > 'heavy' camp (as opposed to the lightweight/agile camp). > > In my own job, which requires writing software for lay users, all I > ever get is abbreviated English language requests, and I have learned > better than to ask users for their requirements because they have no > idea what requirements are. (As a joke, I have sent a couple a copy of > IEEE Std 830-1984 and told them that I needed something like that, but > the joke went over like a lead balloon -- not funny at all.) Of > necessity I have learned to expect to write a number of versions of > the same script before the user accepts it. > > I understand that Graham isn't talking about requirements, and to many > people specifications and requirements amount to the same thing. I > also understand the necessity for planning. However, the Graham quote > seems to me a reasonable articulation for ad hoc development. (It's > something I wanted to say to jue in particular but couldn't find the > words.) > > Comments? > > CC QUOTE You can't write specifications that say exactly what you want. If the specification were that precise, then they would be the program. UNQUOTE That's a very clever and profound observation from Paul Graham. The formal methods people might disagree though. I think the obvious counterexample comes from constructive type theory, where the specification is a type designed to determine the program. But the specification is nevertheless not itself a program. The program emerges as a byproduct of an attempt to prove that the specification can be met (that the type is inhabited). That's not the end of the argument; its just pawn to e4, pawn to e5 in this debate. Mark
From: dan on 16 Feb 2010 17:00 Mark Tarver <dr.mtarver(a)ukonline.co.uk> writes: > QUOTE > You can't write specifications that say exactly what you want. If the > specification > were that precise, then they would be the program. > UNQUOTE > > That's a very clever and profound observation from Paul Graham. The > formal methods people might disagree though. So would I. I would like a program that calculates the number x for which x*x=52 That specification says exactly what I want, but it's of no help at all in creating an algorithm for how to get it. -dan
From: Mark Tarver on 16 Feb 2010 17:13 On 16 Feb, 22:00, d...(a)telent.net wrote: > Mark Tarver <dr.mtar...(a)ukonline.co.uk> writes: > > QUOTE > > You can't write specifications that say exactly what you want. If the > > specification > > were that precise, then they would be the program. > > UNQUOTE > > > That's a very clever and profound observation from Paul Graham. The > > formal methods people might disagree though. > > So would I. > > I would like a program that calculates the number x for which x*x=52 > > That specification says exactly what I want, but it's of no help at all > in creating an algorithm for how to get it. > > -dan Actually, and coincidentally, that's the very example which is used in Constable's book of 25 years ago to introduce CTT via Nuprl. And the specification looks almost exactly like yours. And the program is derived without hacking any code. The book is Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Engelwood Cliffs, NJ, 1986 (with PRL Group). ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz might deliver it up. Mark
From: Mark Tarver on 16 Feb 2010 17:44 On 16 Feb, 22:13, Mark Tarver <dr.mtar...(a)ukonline.co.uk> wrote: > On 16 Feb, 22:00, d...(a)telent.net wrote: > > > > > > > Mark Tarver <dr.mtar...(a)ukonline.co.uk> writes: > > > QUOTE > > > You can't write specifications that say exactly what you want. If the > > > specification > > > were that precise, then they would be the program. > > > UNQUOTE > > > > That's a very clever and profound observation from Paul Graham. The > > > formal methods people might disagree though. > > > So would I. > > > I would like a program that calculates the number x for which x*x=52 > > > That specification says exactly what I want, but it's of no help at all > > in creating an algorithm for how to get it. > > > -dan > > Actually, and coincidentally, that's the very example which is used in > Constable's book of 25 years ago to introduce CTT via Nuprl. And the > specification looks almost exactly like yours. And the program is > derived without hacking any code. > The book is > > Implementing Mathematics with the Nuprl Proof Development System. > Prentice-Hall, Engelwood Cliffs, NJ, 1986 (with PRL Group). > > ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz > > might deliver it up. > > Mark- Hide quoted text - > > - Show quoted text - However that said, Graham is 90% right. You just have to reformulate what he says a little from You can't write specifications that say exactly what you want. If the specification were that precise, then they would be the program. to You can't write specifications that say exactly what you want. If the specification were that precise, then they would be the program or as long as the program. And that's about right. But there is not a lot of point in specifications that are as long as the program because then there is as much chance of making an error in the specification as in the program. Hence the specification brings no actual security. Ideally specifications should be 1. Totally determinant of the correctess of the program. 2. Short and dazzingly clear. However these two requirements are generally at odds with one another. If you buy into 'short and dazzingly clear' then your specification will likely underspecify. If you buy into 'totally determinant' then your specification is likely to approach the length of the program. In the case of CTT, when you count in the axioms and rules needed to synthesise a program, the length actually exceeds the length of the program by a wide margin. For instance in my short intro to CTT in Qi, I formally specify and synthesise a program that adds two numbers together - with the aid of 24 pages of math'l logic. http://www.lambdassociates.org/Lib/Logic/Martin-Lof/martin-lof.pdf The lesson to be learned is that though, with great effort, you can reduce programming to a math'l activity but it may not gain in clarity or accuracy from so doing. Mark
From: Ron Garret on 17 Feb 2010 02:21
In article <2f580d01-8f4c-4c08-a6a6-8fc84dd4658e(a)15g2000yqa.googlegroups.com>, Mark Tarver <dr.mtarver(a)ukonline.co.uk> wrote: > QUOTE > You can't write specifications that say exactly what you want. If the > specification were that precise, then they would be the program. > UNQUOTE > > That's a very clever and profound observation from Paul Graham. It is also demonstrably false. > The formal methods people might disagree though. The formal methods people are also wrong, but for different reasons. > I think the obvious counterexample comes from constructive type > theory, where the specification is a type designed to determine the > program. But the specification is nevertheless not itself a program. > The program emerges as a byproduct of an attempt to prove that the > specification can be met (that the type is inhabited). That's not the > end of the argument; its just pawn to e4, pawn to e5 in this debate. You don't have to get anywhere near that esoteric. There are many precise specifications that are nonetheless very hard or impossible to render into code, the classic example being F(X,Y)=TRUE if and only if X is the encoding of a program that halts when run on input Y. Imprecise specifications are only one of many potential challenges to producing code that does what you want. Inverting SHA1, factoring RSA1024, and decrypting AES256 are all specifications that can be rendered with absolute precision. But that will not help you at all when it comes time to code them up. rg |