Re: "Perfect" or "Provable" security both crypto and non-crypto?

From: David Wagner (daw_at_taverner.cs.berkeley.edu)
Date: 09/15/04 

Date: Tue, 14 Sep 2004 22:13:17 +0000 (UTC)

Douglas A. Gwyn wrote:
>It is not a problem with the techniques I was talking about,
>which can and should be taught throughout the education of
>programmers.

Do you have any evidence that one can successfully teach Hoare logic,
weakest preconditions, and the like in entry-level programming classes?
I'll believe it when I see it, but in the meantime, I'll be skeptical --
that claim doesn't mesh with my experience. At that level, many people
are still struggling with concepts like big-Oh notation, and formal
logic requires quite a bit more mathematical sophistication than that.
I'm afraid many of our programmers are never going to be math experts,
and may never understand the intricacies of first-order logic.

As for cost, it seems to me that in principle the question to ask is
pretty natural: Do the benefits of formal verification (e.g., fewer bugs)
exceed the costs? Right now, for most software the answer is a clear and
resounding "No". For most widely used commercial off-the-shelf software,
the costs (to developers) greatly exceed the benefits (to developers).

Now if you want to talk about specialized arenas, like control systems
for aircraft or nuclear power plants, the answer may well be different.
I don't know. But when it comes to commercial software, the answer is
all too clear: formal verification is too expensive. I wish it weren't
so, but I don't know how to get around it.

As I said before, if you have a counterexample, feel free to produce it.
I'd be totally overjoyed to be proven wrong -- it'd be great if there
were some nice solution here. However, it seems to me you're making an
extraordinary claim, and I haven't seen any evidence for it. (It's often
said that extraordinary claims require extraordinary evidence, but I'd
settle for even mediocre evidence.)

Relevant Pages

  • Re: Private Parking Fine
    ... I invite them to provide me with copies of any evidence they intend to rely ... Courts don't like cases with no evidence, and it either won't get to court ... two over-zealous police officers, even though the RAC had advised that it ... ordered the barrister's costs to be paid by the police. ...
    (uk.legal)
  • Re: Athesists
    ... the more extraordinary the evidence will have to be to convince me. ... BillB makes the extraordinary claim that he won $10,000 playing penny ante poker ... ... So, you made $10,000 playing low limit. ... "After I won him $5000 playing low limit I was convinced, and switched to my own account." ...
    (rec.gambling.poker)
  • Re: Athesists
    ... the more extraordinary the evidence will have ... BillB makes the extraordinary claim that he won $10,000 ... So, you made $10,000 playing low limit. ... evidence will have to be to convince me." ...
    (rec.gambling.poker)
  • Re: ILADS guidelines now online
    ... First WHAT COSTS? ... >> guidelines with money and they wanted their money back! ... > Do you think there exists evidence to support the recommendations? ... refers to published reports of experiences in clinical practice rather ...
    (sci.med.diseases.lyme)
  • Re: OT - Chicago No Trump
    ... is no evidence whatever that medical practices are better due to the ... There is plenty of evidence that the enormous ... carry the highest such costs. ... to repair injuries resulting from poor or negligent practice. ...
    (rec.music.opera)
Quantcast