PEP 3107 and stronger typing (note: probably a newbie question)

[Paul Rubin]

"Chris Mellon" <arkanes at gmail.com> 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.