tough-to-explain Python

[Simon Forman]

On Jul 20, 4:00 am, greg <g... at cosc.canterbury.ac.nz> wrote:
> Calroc wrote:
> > It may be that flawless software is an unreachable asymptote, like the
> > speed of light for matter, but I'm (recently!) convinced that it's a
> > goal worthy of exploration and effort.
>
> Seems to me that once you get beyond the toy program
> stage and try to apply correctness proving to real
> world programming problems, you run up against the
> problem of what exactly you mean by "correct".
>
> Once the requirements get beyond a certain level of
> complexity, deciding whether the specifications
> themselves are correct becomes just as difficult as
> deciding whether the program meets them.

I agree.  You could prove that a game renders geometry without
crashing, but not that it's fun.  Or in an accounting package you
could prove that it never loses a cent in tracking accounts and
payments, or that its graph-rendering code does correctly render data
(without introducing artifacts, for instance), but not that it will
let you notice trends.

> Then there's the fact that very often we don't
> even know what the exact requirements are, and it's
> only by trying to write and use the program that
> we discover what they really are -- or at least,
> get a better idea of what they are, because the
> process is usually iterative, with no clear end
> point.

Aye, if you're still exploring your solution space your requirements
are perforce somewhat nebulous.

> So in theory, correctness proofs are a fine idea,
> and might even be doble on a small scale, but the
> real world is huge and messy!

Very true, but I think it is still worthy to build larger systems from
proven components combined in provably correct ways, at least to the
extent possible.

> > Just because it's unattainable doesn't make it undesirable.  And who
> > knows? Maybe the horse will learn to sing.
>
> Striving to find ways of writing less bugs is a
> worthy goal, but I think of it more in terms of
> adopting patterns of thought and programming that
> make it more likely you will write code that does
> what you had in mind, rather than a separate
> "proof" process that you go through afterwards.

I would consider formal methods exactly "patterns of thought and
programming that make it more likely you will write code that does
what you had in mind", in fact that's why I'm excited about them.

My understanding (so far) is that you (hope to) /derive/ correct code
using formal logic, rather than writing code and then proving its
soundness.

The real win, IMO, is teaching computers as a logical, mathematical
activity (that can certainly depart for realms less rigorously
defined.)

I think anyone who can spontaneously solve a Sudoku puzzle has enough
native grasp of "formal" methods of reasoning to learn how to derive
working programs logically.  Making the formal methods explicit gives
you the strongest available confidence that you are reasoning, and
programming, correctly.

This is not to say that "incorrect" (or unproven or unprovable)
programs are never useful or necessary.  However, I do feel that it's
better to learn the "correct" way, and then introduce ambiguity, than
to simply throw e.g. Java at some poor student and let them find solid
ground "catch as catch can".


~Simon