tough-to-explain Python

[Simon Forman]

http://dwheeler.com/essays/high-assurance-floss.html

might be an interesting place to start.

OO la la! Thank you!

 

[greg]

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.

 

[Paul Rubin]

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.