4 ms·

This part confused me: "My job is to go beyond correctness, to an analysis of such things as the program's running time: I write down a recurrence, say, which

by jbapple 12y ago

This part confused me: "My job is to go beyond correctness, to an analysis of such things as the program's running time: I write down a recurrence, say, which is supposed to represent the average number of comparisons made by that program on random input data. I'm 100% sure that my recurrence correctly describes the program's performance, and all of my colleagues agree with me that the recurrence is "obviously" valid. Yet I have no formal tools by which I can prove that my recurrence is right. I don't really understand my reasoning processes at all! My student Lyle Ramshaw began to create suitable foundations in his thesis (1979), but the problem seems inherently difficult." There are formal tools to prove recurrences are correct. First, any proof assistant like Coq or Isabelle could be used to verify recurrences. Papers like "A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq" show that this is not limited to just the recurrence, but can also be applied to programs and random input data. The Certified Complexity (CerCo) project does similar work. Maybe I misunderstood what Knuth meant by "formal tools" or "recurrence is right". Here is a link to the abstract of Ramshaw's thesis: http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=html&identifier=ADA086916 http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=ht...

pavpanchekha 12y ago
I think there is a bit of a disconnect here between the old guard of verification work and the avant-garde. Partly this is a difference of tools and terminology—current work in verification has a type-theory feel, and Floyd-style axiomatic semantics are out of vogue. It is also the role of old professors to slowly lose currency with the cutting edge of a field. I wouldn't think too much of Knuth's comments.
acqq 12y ago
I think you misunderstood him. I believe he knows he can prove that the recurrence finishes, he can't prove that the recurrence he writes is the mathematically right description of the problem he observes.

by jbapple 12y ago

pavpanchekha 12y ago

I think there is a bit of a disconnect here between the old guard of verification work and the avant-garde. Partly this is a difference of tools and terminology—current work in verification has a type-theory feel, and Floyd-style axiomatic semantics are out of vogue. It is also the role of old professors to slowly lose currency with the cutting edge of a field. I wouldn't think too much of Knuth's comments.

acqq 12y ago

I think you misunderstood him. I believe he knows he can prove that the recurrence finishes, he can't prove that the recurrence he writes is the mathematically right description of the problem he observes.