greg <g...@cosc.canterbury.ac.nz> writes: > 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.
Really, it's easier to write specifications. They're a level of abstraction away from the implementation. Think of a sorting function that operates on a list a1,a2...a_n. The sorting algorithm might be some fiendishly clever, hyper-optimized hybrid of quicksort, heapsort, timsort, burstsort, and 52-pickup. It might be thousands of lines of intricate code that looks like it could break at the slightest glance. The specification simply says the output has the property a1<=a2<=...<=a_n. That is a lot easier to say. If you can then prove that the program satisfies the specification, you are far better off than if you have some super-complex pile of code that appears to sort when you test it, but has any number of possible edge cases that you didn't figure out needed testing. It's like the difference between stating a mathematical theorem (like the four-color theorem) and proving it. -- http://mail.python.org/mailman/listinfo/python-list