subbukk <subbukk at gmail.com> writes:
> On Sunday 27 May 2007 1:32 am, Lex Spoon wrote:
> > 1. 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.



> > 2. 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