subbukk subbukk@gmail.com writes:
On Sunday 27 May 2007 1:32 am, Lex Spoon wrote:
- Even when you are thinking about formal proof, like Dijkstra was, parallelism in large OO programs means you have to reason about aliasing, i.e. you have to do data flow analysis. This is hard, probably too hard if the language is unconstrained.
What is hard about programming is coming up with the right invariants. What happens between the starting invariant and ending invariant is determined by the semantics. E.g. x, y := y, x is easier to reason about than bringing in a temp to swap x and y.
An interesting example. This one is about parallelism, but not non-determinism. A generalization would be "clocked" systems, which indeed are really cool.
- Most programs are not formally proven.
True. Proving large programs automatically is theoretically infeasible for most languages in use today. But many algorithms do go thru formal proofs before adoption - e.g. floating point math, semaphores, regular expressions are all based on proven algorithms.
Yes, algorithms are more amenable to proof than implementation. If you implement a proven algorithm, and something goes wrong, then it's a normal old bug. If you do like Java and implement an unproven type system, then you can get really nasty surprises. The last I heard, it is still not even known if Java's generics *can* be fully implemented to spec. That is not a nice place to be as a programmer!
The language question you raise is also interesting. Sometimes implementation languages are pointlessly difficult to prove things about. Other times, though, there is a real tradeoff between implementation speed and provability. A good example is inheritance plus method override. These are really great for adding functionality to existing programs, but are awkward for proof tools because the meaning of a method call depends on which overridden versions of the method you have loaded.
It would be really neat to have a subset of Squeak that was designed to be amenable to proof, and then to teach one of the existing proof systems about this subset. If you include blocks, but reject inheritance, then you could come up with something close to the lambda-calculus-like languages that the existing proof tools are so good at. You would not like programming this way, compared to using full Squeak, but for core things like Semaphore and SharedQueue it would seem useful.
Lex