Re: Blowfish Sign Extension implementation risk

From: Michael Amling (nospam_at_nospam.com)
Date: 04/29/04 

Date: Thu, 29 Apr 2004 11:44:26 GMT

Thomas Pornin wrote:
>
> Some people work on proofs of program correctness: these are automatic
> tools that analyze source code in some language, and establish formally
> that the source code complies with a formal description such as the
> one described above (or point out bugs). Last I heard of it, it can be
> made to work quite effectively with some languages (mostly Lisp-like or
> SML-like); with more low-level languages like C, there is still some
> work to do.
>
> The main problems with that approach are:
> [...]
> -- the problem of correctness is only moved to the problem of making
> sure that the program used to verify the proof is itself correct(**).

   Not to mention the problem of whether the specification that the
program is proven to correctly implement is in fact an accurate
depiction of what the user wants.

--Mike Amling

Relevant Pages

  • Re: How to name variables in a program?
    ... So its an explicit encoding, ... We are also trained to read natural language as well. ... fact even beyond conventions it leads people to write abbreviations on ... > making the whole source code much harder to read. ...
    (comp.programming)
  • Re: RFCAS - Configuration segments in the San language
    ... > San is a new language that I am developing the specifications for. ... > finding source code in other files, ... > and does not work well with code supporting alternate features. ...
    (comp.programming)
  • Re: Programming to Beat the Odds in Gaming
    ... black-red) strategy is no better than straight-red or straight-black. ... don't even know language it is written in. ... In this pseudo-language, a program consists of functions, and a function ... I still haven't seen your source code. ...
    (comp.programming)
  • Re: Spanish characters in Cobol-how to?
    ... Frank Swarbrick wrote: ... language dependent, with a key containing the language, and the ... machine-to-human messages and call a message handler. ... But if the messages are not in the source code this seems ...
    (comp.lang.cobol)
  • Re: BASIC-E
    ... files and found the source code listing for what we then titled "BASICI1". ... I looked at my IMSAI archives and reviewed a few relevant manuals. ... immediate reference to source language. ...
    (comp.os.cpm)