Simon Forman wrote:
My understanding (so far) is that you (hope to) /derive/ correct code using formal logic, rather than writing code and then proving its soundness.
But to the extent you can rigorously formalise it, all you've done is create Yet Another Programming Language. Which is fine, if you can come up with one that works at a high enough level in some domain that you can see just by looking that the program will do what you want. However, I suspect that you can't improve much on what we've already got without restricting the domain of applicability of the language. Otherwise, you just shift the intellectual bottleneck from writing a correct program to writing correct specifications. In the realm of programming language design, it's been said that you can't eliminate complexity, all you can do is push it around from one place to another. I suspect something similar applies to the difficulty of writing programs. -- Greg -- http://mail.python.org/mailman/listinfo/python-list