[tor-talk] BitMail.sf.net v 0.6 - Secure Encrypting Email Client

Robert J. Hansen rjh at sixdemonbag.org
Mon Nov 18 12:30:47 CET 2013

On 11/18/2013 1:52 AM, Johan Wevers wrote:
> Dijkstra's goal of formally prooving entire programs more complicated
> than hello world seems further away than ever. Don't loose any sleep
> over it, noone even tried that in practice anyway.

Well, yes and no.  Provably-correct software is still a very hot thing
in engineering, particularly in life-critical applications like avionics
or nuclear reactor control software.  The Ada programming language has a
couple of variants -- SPARK and its descendants -- that support provable

The problem with provably correct code is that it only proves the code
correctly implements the specification.  It doesn't prove the
specification completely encapsulates the problem...

More information about the Gnupg-users mailing list