"Chris Mellon" <[EMAIL PROTECTED]> writes: > You can't prove a program to be correct, in the sense that it's proven > to do what it's supposed to do and only what it's supposed to do. You > can prove type-correctness, and the debate is really over the extent > that a type-correct program is also behavior-correct.
But every mathematical theorem corresponds to a type, so if you can formalize an argument that your code has a certain behavior, then a type checker can statically verify it. There are starting to be programming languages with embedded proof assistants, like Concoqtion (google for it). Of course you can only prove formal properties of programs, which says nothing about whether the application is doing the right thing for what the user needs. However, you're still way ahead of the game if you have a machine-checked mathematical proof that (say) your multi-threaded program never deadlocks or clobbers data through race conditions, instead of merely a bunch of test runs in which you didn't observe deadlock or clobbered data. Similarly for things like floating-point arithmetic, Intel and AMD now use formal verification on their designs, apparently unlike in the days of the notorious original Pentium FDIV implementation, which passed billions of test vectors and then shipped with an error. Larger applications like the Javacard bytecode interpreter have been certified for various properties and pretty soon we may start seeing certified compilers and OS kernels. Things have come a long way since the 1970's. > Personally, I remain unconvinced, but am open to evidence - I've only > heard anecdotes which are readily discounted by other anecdotes. I > absolutely do not believe that pure functional style programming, > where we shun variables, is the best model for computing, either now > or in the future. I wonder if you looked at the Tim Sweeney presentation that I linked to a few times upthread. -- http://mail.python.org/mailman/listinfo/python-list
