> I do have a systematic tendency as a teacher and student formerly of > philosophy who entered the computer racket 30 years ago as a > draft-dodging scheme, to bring humanistic interpretation into the > field, and to me CAR and CDR are representative of a tendency in LISP > (please be advised that I have no special expertise in Lisp).
> This is to tie the language, at a key point, to the vendor's hardware. > It was also done in Fortran about the same time.
> Whereas the Algol group pioneered what has turned out to be a better > approach, and that is for a quasi-civic agency to be technically > independent of computer vendors. The Algol team devised the father of > most usable modern languages including C because as an independent > civic forum, they were immune to commercial pressures.
Now here is a gem - someone who doesn't like Lisp because it is too commercial.
Erann Gat wrote: > In article <avd5dm$34...@newsreader2.netcologne.de>, Pascal Costanza > <costa...@web.de> wrote: >>A test ultimately proves that the program is >>correct for the given test suite, and sometimes this is as good as it >>gets.
> In multithreaded or embedded systems the behavior of a program can be > different on multiple runs even when the initial conditions are as similar > as you can possibly make them.
OK, I stand corrected in this regard.
> You can never be 100% sure a system is > bug-free, but the more different kinds if ways you express and cross-check > your intentions the better your chances of getting what you want.
I agree. The important point is to gain different perspectives on the same domain.
Pascal
-- Pascal Costanza University of Bonn mailto:costa...@web.de Institute of Computer Science III http://www.pascalcostanza.de Römerstr. 164, D-53117 Bonn (Germany)
Pascal Costanza <costa...@web.de> writes: > I think that it's a big mistake to trust any kind of method more than > to trust human beings. If someone says that they have applied rigorous > mathematical methods and are certain by now that their system works, > then you show trust in them (or their judgement) and not in those > methods. That's the way it should be IMHO.
But what if the human is at odds with the mathematical result? Then what/who do you trust?
>>>>> "EN" == Erik Naggum <e...@erik.naggum.no> writes:
EN> But let us have another row over rudeness, again. They're EN> /fun/!
Actually, for the record, I like rows over rudeness, because some of the vitriol is worth rereading several times. Interesting discussion of LISP would be preferable, of course, but rows over rudeness are far more entertaining than yet another round of 'cn u h3lp m3 wif my h0mew0rk?'
IMO, the interest of formal proof of programs is not so much as an alternative to test cases than as a step to automatic generation/verification of program.
That is, an informal specification, an informal program construction and some informally developped test cases, as done by human programmers can show that in some cases the program written is correct, and the programmer can even have confidence (by his mental process while constructing the program) that he wrote a correct program in all the cases specified.
But until we have a strong AI, this cannot be reproduced automatically (and anyway, check the current software quality to see what results are attained this way).
If instead we start from formal specifications and formal software development and verification, this can be implemented in software with a set of tools that don't amount to strong AI: theorem proovers, theorem checkers, program generators, some goal directed search, etc, that could be implemented today.
I know that it's proven that no program can prove the termination in general. But if you check carefully, you'll see that to prove this theorem, we apply termination prover on itself. So we just found an example, a case where it's not possible, but it does not mean that this program cannot be helpful to analyse and verify the other programs. By the way, have you ever found a programmer capable of proving that for any specification he can himself generate a correct program in finite time? (Since he has no formal specifications of his own brains, he would have quite some difficulties to start such a proof).
Now, once we have software programmers, I agree that bug could still be generated. Like in our informal world, where to err is human, perhaps to err will be software too (while I hope they'll err less). The difference is that once a bug is detected you need to stop everything and start a laborious debugging/develop/test cycle before installing a new version. A software formally developped automatically could be monitored by AI agents and the debugging/correction of the formal specification or of the formal proof/regeneration of software/formal verification (and perhaps automatic generation and run of test cases to make everybody happy), could be implemented and run automatically, reducing the down time.
-- __Pascal_Bourguignon__ http://www.informatimago.com/ ---------------------------------------------------------------------- There is a fault in reality. Do not adjust your minds. -- Salman Rushdie
* Pascal Bourguignon | But until we have a strong AI, this cannot be reproduced automatically | (and anyway, check the current software quality to see what results | are attained this way).
While the root cause of crime is obviously the laws, it really sounds like you believe that the system is to blame for individual failures.
| If instead we start from formal specifications and formal software | development and verification, this can be implemented in software | with a set of tools that don't amount to strong AI: theorem | proovers, theorem checkers, program generators, some goal directed | search, etc, that could be implemented today.
Before you do this, you should to try give some program a program and wait for it to tell you what that program actually does.
| (Since he has no formal specifications of his own brains, he would | have quite some difficulties to start such a proof).
Do you really believe such hogwash or are you just pretending to be stupid for its effect?
| Like in our informal world, where to err is human, perhaps to err | will be software too (while I hope they'll err less).
You really have no idea what "to err is human" means, do you?
I occasionally entertain a Microsoft "fan" with a discussion on the real problem behind viruses and malicious abuse of their software. I maintain that the problem is not that the software is not perfect or approved or proven correct or any such thing, but that it is not /defensive/ against harmful data. There are basically two ways to build a society of autonomous units: You either design away all the anti-social flaws from the outset and let them go their happy way, or you design every single unit with an /immune system/ that copes with bad guys if and when they exist. The problem is therefore not that some software gets viruses or rotten data, but that it keeps going as if it were completely unaffected by it.
Drop the moronic "proof of correctness" and "verification" nonsense and design systems that can actually defend themself from bad input.
-- Erik Naggum, Oslo, Norway
Act from reason, and failure makes you rethink and study harder. Act from faith, and failure makes you blame someone and push harder.
Pascal Bourguignon <p...@informatimago.com> writes: > I know that it's proven that no program can prove the termination in > general. But if you check carefully, you'll see that to prove this > theorem, we apply termination prover on itself. So we just found an > example, a case where it's not possible, but it does not mean that > this program cannot be helpful to analyse and verify the other > programs.
Many programmers are under the impression that although non-termination is impossible to determine in general, that it is probably determinable in practice, or at least in a large enough set of cases as to be useful. This isn't true.
It is quite easy to find very simple programs that cannot be proven to terminate, and they come up in practice far more often than you'd think. Here is an artificial one I came up with:
(defun kernel (s i) (list (not (car s)) (if (car s) (cadr s) (cons i (cadr s))) (cons 'y (cons i (cons 'z (caddr s))))))
The kernel function trivially terminates, the call to reduce terminates, the list over which mystery iterates is finite for all iterations, yet it is not known whether mystery terminates for all finite lists. (Google on `Collatz Problem' for details.)
The reason I coded this is because the only obstacle to termination analysis appears to be the iteration in `mystery'. Yet iterations such as this are not an uncommon feature in typical programs.
you well see some examples where Godel's incompleteness theorem (related to the halting problem) has cropped up in several `natural independence phenomena' that don't require the trick of attempting to apply a proof to itself. One of the problems is `Kruskal's tree theorem' that is involved in showing that certain orderings on trees are well-founded.
Again, tree traversal is a common programming technique.
Joe Marshall <j...@ccs.neu.edu> writes: > Matthew Danish <mdan...@andrew.cmu.edu> writes:
> > I have asked this very question on this newsgroup before: What would be > > a better name for CAR and CDR?
> MOM and DAD?
The neat thing about CAR and CDR is that they start and end with the same letter, AND one has a vowel and the other has a consonant. That lets you do the CADAR trick and have a good chance that it will be pronounceable. I think Lisp got lucky with CAR and CDR.
Just because something's old and takes a little getting used to doesn't mean it's bad.
-- Fred Gilham gil...@csl.sri.com And then [Clinton] turned to Hunter Thompson, of all people, and said with wholehearted fervor, "We're going to put one hundred thousand new police officers on the street." I was up all night persuading Hunter that this was not a personal threat. -- P. J. O'Rourke
In article <smw3fui3....@ccs.neu.edu>, Joe Marshall <j...@ccs.neu.edu> wrote: > Pascal Bourguignon <p...@informatimago.com> writes:
> > I know that it's proven that no program can prove the termination in > > general. But if you check carefully, you'll see that to prove this > > theorem, we apply termination prover on itself. So we just found an > > example, a case where it's not possible, but it does not mean that > > this program cannot be helpful to analyse and verify the other > > programs.
> Many programmers are under the impression that although > non-termination is impossible to determine in general, that it is > probably determinable in practice, or at least in a large enough set > of cases as to be useful. This isn't true.
> It is quite easy to find very simple programs that cannot be proven to > terminate, and they come up in practice far more often than you'd > think. Here is an artificial one I came up with:
This is a fallacious argument. Your claim (slightly refactored) is that it is not possible to determine whether or not a program halts in a significant of useful cases. But you support for this claim is that no general proof is known for a particular (and rather artificial IMO) case. That seems like a non-sequitur to me at best. That's like trying to disprove that *most* (not all) crows are black by exhibiting a white crow.
Nonetheless, the references you point to make fascinating reading.
> > > I know that it's proven that no program can prove the termination in > > > general. But if you check carefully, you'll see that to prove this > > > theorem, we apply termination prover on itself. So we just found an > > > example, a case where it's not possible, but it does not mean that > > > this program cannot be helpful to analyse and verify the other > > > programs.
> > Many programmers are under the impression that although > > non-termination is impossible to determine in general, that it is > > probably determinable in practice, or at least in a large enough set > > of cases as to be useful. This isn't true.
> > It is quite easy to find very simple programs that cannot be proven to > > terminate, and they come up in practice far more often than you'd > > think. Here is an artificial one I came up with:
> This is a fallacious argument. Your claim (slightly refactored) is that > it is not possible to determine whether or not a program halts in a > significant of useful cases. But you support for this claim is that no > general proof is known for a particular (and rather artificial IMO) case.
The reason I don't think it is completely fallacious is that I don't think the example is too artificial. The proof that a termination prover fails upon itself seems extreme in that how often does one reason about termination provers? The example I gave was one that involved very simple functions like CONS, CAR, CDR, EQ, DO, and REDUCE, and used them in a way that (at least to me) doesn't seem unusual.
> That seems like a non-sequitur to me at best.
It may be a bit of leap, so let me fill in the gaps:
Assume that it *is* possible to determine whether or not a program halts in virtually every useful case.
Therefore, an undecidable program must be out of the ordinary.
But the program exhibited *is* ordinary.
So my argument hinges on whether or not you think my example case is ordinary. (and as you indicated above, you don't) Now, for the sake of pushing the point, exactly what is it about my example case, aside from being undecidable, that pushes beyond the realm of `ordinary' into `extraordinary'?
> That's like trying to disprove that *most* (not all) crows are black > by exhibiting a white crow.
Well, the original argument was like:
`The fact that all crows are black is disproved by this mutant crow, but that's a special case. A lot of `normal' crows are black.'
to which I responded:
`This crow isn't black, and it doesn't seem to be mutant. Looks a lot like any other crow other than the color. I see no reason why crows like this should be rare.'
But there is a small problem with the analogy: the color of a crow is readily apparent. The question of whether or not an interesting set of programs terminate is not (and in fact, the question under debate).
> > That's like trying to disprove that *most* (not all) crows are black > > by exhibiting a white crow.
> Well, the original argument was like:
> `The fact that all crows are black is disproved by this mutant > crow, but that's a special case. A lot of `normal' crows are > black.'
> to which I responded:
> `This crow isn't black, and it doesn't seem to be mutant. Looks a > lot like any other crow other than the color. I see no reason > why crows like this should be rare.'
> > > > I know that it's proven that no program can prove the termination in > > > > general. But if you check carefully, you'll see that to prove this > > > > theorem, we apply termination prover on itself. So we just found an > > > > example, a case where it's not possible, but it does not mean that > > > > this program cannot be helpful to analyse and verify the other > > > > programs.
> > > Many programmers are under the impression that although > > > non-termination is impossible to determine in general, that it is > > > probably determinable in practice, or at least in a large enough set > > > of cases as to be useful. This isn't true.
> > > It is quite easy to find very simple programs that cannot be proven to > > > terminate, and they come up in practice far more often than you'd > > > think. Here is an artificial one I came up with:
> > This is a fallacious argument. Your claim (slightly refactored) is that > > it is not possible to determine whether or not a program halts in a > > significant of useful cases. But you support for this claim is that no > > general proof is known for a particular (and rather artificial IMO) case.
> The reason I don't think it is completely fallacious is that I don't > think the example is too artificial.
Even if the example is not artificial, one counterexample does not refute a non-universal claim.
It may be that, say, half of all programs are amenable to some kind of formal proof of correctness, and half are not. I'd say that half of all cases is a "large enough set to be useful." But there would still be no sport in finding counterexamples.
> The example I gave was one that > involved very simple functions like CONS, CAR, CDR, EQ, DO, and > REDUCE, and used them in a way that (at least to me) doesn't seem > unusual.
But it doesn't do anything useful.
> It may be a bit of leap, so let me fill in the gaps:
> Assume that it *is* possible to determine whether or not a program > halts in virtually every useful case.
That wasn't the claim. The claim was "a large enough subset to be useful", not "virtually every useful case."
Joe Marshall <j...@ccs.neu.edu> writes: > Pascal Bourguignon <p...@informatimago.com> writes:
> > I know that it's proven that no program can prove the termination in > > general. But if you check carefully, you'll see that to prove this > > theorem, we apply termination prover on itself. So we just found an > > example, a case where it's not possible, but it does not mean that > > this program cannot be helpful to analyse and verify the other > > programs.
> Many programmers are under the impression that although > non-termination is impossible to determine in general, that it is > probably determinable in practice, or at least in a large enough set > of cases as to be useful. This isn't true.
> It is quite easy to find very simple programs that cannot be proven to > terminate, and they come up in practice far more often than you'd > think. Here is an artificial one I came up with:
> The kernel function trivially terminates, the call to reduce > terminates, the list over which mystery iterates is finite for all > iterations, yet it is not known whether mystery terminates for all > finite lists. (Google on `Collatz Problem' for details.)
Yes, it's similar to this numerical function:
(defun hotpo (n) ;; hotpo stands for Half Or Triple Plus One (cond ((= n 1) t) ((oddp n) (hotpo (+ 1 (* n 3)))) (t (hotpo (/ n 2)))))
Well, I must say that in 28 years of programming, this is the only function that I wrote that don't obviously terminate. (I think I proved a few years ago that it terminates though). While I must confess that I didn't prove the termination of most of my functions, I would be very happy to have an automatic prover to check my simple algorithms.
> The reason I coded this is because the only obstacle to termination > analysis appears to be the iteration in `mystery'. Yet iterations > such as this are not an uncommon feature in typical programs.
"typical programs" in what domain? For 90% of the application domains and 99.99% for the programs, such algorithms don't occur, or are avoided just because there are alternatives whose termination is more obvious. (percentages invented here, but serriously, think about all these business or desktop applications that could be much less bugged if automatic tools was disponible to work on them).
> you well see some examples where Godel's incompleteness theorem > (related to the halting problem) has cropped up in several `natural > independence phenomena' that don't require the trick of attempting to > apply a proof to itself. One of the problems is `Kruskal's tree > theorem' that is involved in showing that certain orderings on trees > are well-founded.
> Again, tree traversal is a common programming technique.
-- __Pascal_Bourguignon__ http://www.informatimago.com/ ---------------------------------------------------------------------- There is a fault in reality. Do not adjust your minds. -- Salman Rushdie
faust <urfa...@optushome.com.au> writes: > >> > I have asked this very question on this newsgroup before: What would be > >> > a better name for CAR and CDR?
> >> MOM and DAD?
> >The neat thing about CAR and CDR is that they start and end with the > >same letter, AND one has a vowel and the other has a consonant.
> FAT and FART ?
> giving : > FARFATFAR or FATTRTRTRTR
I don't think so.
(CAR (CDR (CAR X))) = (CADAR X)
By analogy your version would be
(FAT (FART (FAT X))) = (FAARAT X)
It would be pronounced Fa-ar-at. It would have kind of a middle-eastern ring to it....
:-)
-- Fred Gilham gil...@csl.sri.com The vicissitudes of history, however, have not dissuaded them from their earnest search for a "third way" between socialism and capitalism, namely socialism. --- Fr. Richard John Neuhaus
In article <87n0ma76ou....@thalassa.informatimago.com>, Pascal Bourguignon
<p...@informatimago.com> wrote: > Yes, it's similar to this numerical function:
> (defun hotpo (n) > ;; hotpo stands for Half Or Triple Plus One > (cond > ((= n 1) t) > ((oddp n) (hotpo (+ 1 (* n 3)))) > (t (hotpo (/ n 2)))))
> Well, I must say that in 28 years of programming, this is the only > function that I wrote that don't obviously terminate. (I think I > proved a few years ago that it terminates though).
I doubt it. If you really proved it that would make you a candidate for the Fields medal. You'd probably remember that.
> In article <87n0ma76ou....@thalassa.informatimago.com>, Pascal Bourguignon > <p...@informatimago.com> wrote:
> > Yes, it's similar to this numerical function:
> > (defun hotpo (n) > > ;; hotpo stands for Half Or Triple Plus One > > (cond > > ((= n 1) t) > > ((oddp n) (hotpo (+ 1 (* n 3)))) > > (t (hotpo (/ n 2)))))
> > Well, I must say that in 28 years of programming, this is the only > > function that I wrote that don't obviously terminate. (I think I > > proved a few years ago that it terminates though).
> I doubt it. If you really proved it that would make you a candidate for > the Fields medal. You'd probably remember that.
If i remember correct it is called "Ulam's suggestion". He assumed that this function terminates but AFAIK none was able to show a proof. But maybe Pascal has solved it ;-)
g...@jpl.nasa.gov (Erann Gat) writes: > It may be that, say, half of all programs are amenable to some kind of > formal proof of correctness, and half are not. I'd say that half of all > cases is a "large enough set to be useful." But there would still be no > sport in finding counterexamples. "Coby Beck" <cb...@mercury.bc.ca> writes:
> Sorry, but these arguments just don't fly.
Ok. I guess I'm unconvincing. Allow me to appeal to algorithmic information theory, then. One of the results of algorithmic information theory is that there is an upper bound on the complexity of a program that a meta-program can reason about. In other words, if you have a program that you use to test terminating conditions, it will be unable to prove termination of programs that are above the algorithmic complexity of the termination prover. (Or to seriously oversimplify, a two page termination tester won't work on programs longer than about two pages.)
In article <7kdef5cm....@ccs.neu.edu>, Joe Marshall <j...@ccs.neu.edu> wrote: > g...@jpl.nasa.gov (Erann Gat) writes:
> > It may be that, say, half of all programs are amenable to some kind of > > formal proof of correctness, and half are not. I'd say that half of all > > cases is a "large enough set to be useful." But there would still be no > > sport in finding counterexamples.
> Ok. I guess I'm unconvincing. Allow me to appeal to algorithmic > information theory, then. One of the results of algorithmic > information theory is that there is an upper bound on the complexity > of a program that a meta-program can reason about.
There is an upper bound on the complexity of programs that meta-programs can reason about *in general*. But that leaves open a wide variety of useful possibilities:
* a subset of programs that obey certain constraints that allow them to be reasoned about
* a reasoner that is not 100% accurate, but which produces only false negatives (i.e. it says "I can't prove this program is correct" when it is in fact correct).
* a method of transforming programs that cannot be reasoned about into ones that can. (Wrapping a timeout around a program is one example of such a transformation).
> In other words, if > you have a program that you use to test terminating conditions, it > will be unable to prove termination of programs that are above the > algorithmic complexity of the termination prover.
No, it will be unable to prove the termination of *some* programs that are above the algorithmic complexity of the prover. The key question is: are the programs that are left useful? That is an open question, but anecdotal evidence indicates that the answer is yes.
g...@jpl.nasa.gov (Erann Gat) writes: > > In other words, if you have a program that you use to test > > terminating conditions, it will be unable to prove termination of > > programs that are above the algorithmic complexity of the > > termination prover.
> No, it will be unable to prove the termination of *some* programs that are > above the algorithmic complexity of the prover.
I think we must be a cross purposes here: if the algorithmic complexity of the prover is small, then it simply doesn't have enough information capacity to make statements about the space of programs larger than itself. If it could, then you could encode the larger programs in terms of the smaller, and contradict the supposition that the program being examined is more complex than the prover.
> The key question is: are the programs that are left useful?
Well, another key question is `Are there very many programs left?'
> That is an open question, but anecdotal evidence indicates that the > answer is yes.
What anecdotes? The anecdotes I've heard say the opposite.
Consider this: you certainly can't prove the termination of any program capable of universal computation. But it is surprisingly easy to perform universal computation, and it often happens that systems that were not designed for universal computation can be coaxed into doing it.
> > I think that it's a big mistake to trust any kind of method more than > > to trust human beings. If someone says that they have applied rigorous > > mathematical methods and are certain by now that their system works, > > then you show trust in them (or their judgement) and not in those > > methods. That's the way it should be IMHO.
> But what if the human is at odds with the mathematical result? Then > what/who do you trust?
