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

[Robert J. Hansen]

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
code.

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...