[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