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

From: Douglas A. Gwyn (DAGwyn_at_null.net)
Date: 09/14/04 

Date: Tue, 14 Sep 2004 19:42:37 GMT

David Wagner wrote:
> Douglas A. Gwyn wrote:
> >David Wagner wrote:
> >> I don't think that's true. A fair number of graduate students here study
> >> Hoare logic, weakest preconditions, and similar material.
> >Unfortunately most programming doesn't seem to be done by postdocs.
> Right. And this demonstrates exactly the problem with these techniques.

It is not a problem with the techniques I was talking about,
which can and should be taught throughout the education of
programmers. If the ones you are talking about are taught
only as academic abstractions, reserved for upper-level
education of those who are not likely to be the ones who
actually produce software, rather than being practical
methods of value in everyday programming, then that is a
problem with academia.

> Today, using these methods requires a great deal of mathematical expertise
> and sophistication -- and even then, it is time-consuming.

The time taken to do something right as opposed to doing
it wrong is relatively negligible in many cases where
important human goals can depend on the correctness.

Note that I'm also including technology such as structured
system specification, which I've been involved in applying
in the development of several very large software systems,
which would have turned out much worse without the extra
effort up front. Indeed, serious software engineers often
observe that the cost of an error is "exponentially" greater
the earlier in the development cycle at which it occurs;
therefore, considerable extra effort is justifiable to
achieve correctness in the early phases of development.

Relevant Pages

  • Re: Response to Karen and to Willem on recursive proofs
    ... > Could you give an example of a correctness proof involving recursion? ... // But since it can be seen by inspection of the loop termination condition ... // Recursion in programming is, of course, a subroutine calling itself. ...
    (comp.programming)
  • Re: Observer pattern limitations
    ... I think that you should better attack the whole comunity using 3GL. ... where there is so little discussion about correctness. ... What is reactive style of programming? ... computational geometry where formalism is required and *expected*. ...
    (comp.object)
  • Re: {newbie} question regarding C++ references
    ... ...which wasn't a significant difference. ... Yeah, the significant part was the correctness, or in your case, the ... programming while avoiding layoffs by using office politics and ... social and work backgrounds doesn't obscure that, ...
    (comp.programming)
  • Re: Theory of programming
    ... All trivial-input programs have an equivalent Turing machine ... > modern programming. ... computer science which isn't in my mind efficiency it is correctness. ...
    (comp.programming)
  • Re: maths for programming C++
    ... Someone who values readability over correctness, ... I'm advocating a programming style that is literate. ... control flow mechanisms I used were FOR/NEXT, GOTO, and IF/THEN GOTO. ...
    (comp.programming)
Loading