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... _______________________________________________ Gnupg-users mailing list Gnupg-users@gnupg.org http://lists.gnupg.org/mailman/listinfo/gnupg-users
