Re: Python from Wise Guy's Viewpoint

From: Pascal Bourguignon (spam_at_thalassa.informatimago.com)
Date: 11/03/03 

Date: 03 Nov 2003 19:27:53 +0100

gat@jpl.nasa.gov (Erann Gat) writes:
>
> Ah, but now you've added an additional constraint, namely, that my spec be
> funcallable. Not all formal specifications can be rendered as functions.
> For example, "This program terminates" can be formally rendered, but not
> as a program.
> [...]
> But that only works if the specification is computable. Not all formal
> specifications are computable. I can render any specification
> uncomputable by adding the stipulation that the program must halt (or that
> it must not halt).

Pragmatically, we don't need a "this program terminates" predicate. I
could write any number of programs that would provably terminate in 20
billion years. Too bad the estimated death of the universe is in 15
billion years. What we need is a "this program terminates before x
seconds". And this can perfectly be programmed. 

-- 
__Pascal_Bourguignon__
http://www.informatimago.com/

Relevant Pages

  • Re: Python from Wise Guys Viewpoint
    ... Not all formal specifications can be rendered as functions. ... I can render any specification ... You also need a predicate like "this program terminates before x*input ...
    (comp.lang.lisp)
  • Re: "Perfect" or "Provable" security both crypto and non-crypto?
    ... > Oops, I blurred the line between having specifications and having ... I should say that specifications are required ... > in regulated industries while formal specifications are not. ... One wishes that more crypto protocols would be ...
    (sci.crypt)