tough-to-explain Python

[Steven D'Aprano]

I think I'll avoid coming to your house for a cup of coffee.

I meant the instant coffee powder is prepared in advance. It's useless on
it's own, but later on you feed it into boiling water, add sugar and
milk, and it's slightly less useless.

 

[D'Arcy J.M. Cain]

I meant the instant coffee powder is prepared in advance. It's useless on
it's own, but later on you feed it into boiling water, add sugar and
milk, and it's slightly less useless.

I don't know about that. I find instant coffee pretty useless no
matter what it is fed to.

 

[pdpi]

I must admit, it never crossed my mind that anyone here would claim that
there was no creativity involved in programming, that it was all a
mindless, algorithmic process capable of being done by a simple
mechanical device.

This is certainly the accusation made against *bad* programmers -- that
they can't actually solve new, unique problems, but just apply recipes
they learned without any insight or intelligence. The sort of people who
program so poorly that "a trained monkey could do what they do".

I wholeheartedly agree. Coming up with Duff's device is nothing if not
creative. My mind still reels at trying to grok it.
http://www.lysator.liu.se/c/duffs-device.html

Even *soup stock* fits the same profile as what Hendrik claims is almost
unique to programming. On its own, soup stock is totally useless. But you
make it, now, so you can you feed it into something else later on.

Or instant coffee.

I've always found cooking an apt metaphor for programming.

You've got your well-limited for loops (cook for x minutes), your less
straightforward while/until loops (roast until golden), you have your
subprocedures (prepare sauce in advance/in parallel), you have some
conditionals (tenderize the steak if the meat isn't really that
tender), etc etc.

The complexities of assignment can be easily visualized in terms of
containers and mixing stuff together. Nothing makes a += b more
obvious than having a bowl of cream (a), an egg (b), and adding the
egg to the bowl of cream (a += b). Well, except for the part where
that in that case evaluating b is destructive

They can't reason? Then what are they doing when they manipulate symbols?

"Computers aren't intelligent. They only think they are." Or, more to
the point: the typical definition of "reasoning" tends to involve more
of what defines humans as self-aware, animate beings than what is
usually ascribed to computers.

 

[Wesley Chun]

I'm having a hard time coming up with a reasonable way to explain
certain things to programming novices.
:
How do I explain to rank beginners (no programming experience at
all) why x and y remain unchanged above, but not z?
:
What do you say to that?

I can come up with much mumbling about pointers and stacks and
heaps and much hand-waving about the underlying this-and-that, but
nothing that sounds even remotely illuminating.

Your suggestions would be much appreciated!

kj,

i don't have too much to add to everyone else's response except to
describe how i deal with this. i teach Python courses several times a
year and realized long ago that conveying the concept of mutable vs.
immutable is a key to getting up-to-speed quickly with Python as well
as helping beginners.

so, although techically, this is more of an intermediate topic rather
than "beginner" material, i still teach it anyway, with the hopes of
producing better Python programmers out of the gate, and hopefully,
less frustrated ones. in fact, i dedicated an entire chapter (4) in
Core Python Programming just to address this important issue. to top
it all off, i end this module in the class by giving 2 quizzes, just
to make sure they understood what i just told them. i put the 1st one
online, so if you're curious, the PDF is at http://roadkill.com/~wesc/cyberweb/introQuiz.pdf
.... the 2nd quiz is harder and involves the discussion of the
differences between shallow and deep copies. so yes, not very beginner-
ish stuff, hence the reason why i (re)named my course "Intro
+Intermediate Python".

finally, rather than the "paper tag" or alex's hotel statue analogy, i
just say that variables are like Post-It® or sticky notes on
objects. i can tag objects anytime, tag objects more than once, remove
tags, or switch them to another object, etc.

just my $0.02,
-- wesley
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
"Core Python Programming", Prentice Hall, (c)2007,2001
"Python Fundamentals", Prentice Hall, (c)2009
http://corepython.com

wesley.j.chun :: wescpy-at-gmail.com
python training and technical consulting
cyberweb.consulting : silicon valley, ca
http://cyberwebconsulting.com

 

[Terry Reedy]

This is *not* a bug in Bentley's program.

Wow. That's an impressive set of typos

3. Way beneath my usual standards ;-)

Is binary search *supposed* to raise an overflow error if given more than
2**30 elements?

No. it is supposed to work, and Bentley's program will work if lo and hi
are actually integers, as his program presupposes, and not residue
classes mislabeled 'int'.

Is there something special about OverflowError that is "better" than
ArrayIndexOutOfBoundsException?

Wrong comparison. The actual alternative to OverflowError is a negative
number as the sum of two positive numbers. If one claims that a and b
are positive ints, then returning a negative is a bug. The index
exception was a side effect, in Java, of using the negative as an index.
In C, the side effect was a segmentation fault. Do you seriously
question that OverflowError is better than seg faulting? A different
program could go on to silently return a wrong answer. Perhaps it would
say to go west instead of east, or to reduce a medical dosage instead of
raising it.

Note that negative ints are legal indexes in Python, so that if any
Python version ever had ints that wrapped instead of overflowing or
returning a long, then the program would not necessarily stop.

but there's no reason to imagine that the book will assume -- or even
state as a requirement for binary search -- that addition will never
overflow.

Bentley assumed that if (lo+hi)/2 were successfully calculated, then it
would be a positive number between lo and hi, and therefore a legal index.

The dirty secret of computing is that some languages do not have integer
types. They do not even have restricted-range integer types, which would
noisily fail when they cannot perform an operation. They only have
residue class types, which are something else, and which can give
bizarre results if one mindlessly uses them as if they really were
restricted-range integers. When one wants integer operations, every
operation with two residue-class variables has a potential *silent* bug.
Being relieved of the burden of constantly keeping this in mind is one
reason I use Python.

Float types are usually restricted range types. A huge_float +
huge_float may raise overflow, but never returns a negative float.

Bentley assumed that indexes hi and lo are integers. If one uses
restricted range integers that are too large, then lo+hi could fail
gracefully with an appropriate effor message. I would not consider that
a bug, bug a limitation due to using limited-range numbers. If one uses
residue classes instead of integers, and makes no adjustment, I consider
it wrong to blame Bentley.

Terry Jan Reedy

 

[Terry Reedy]

But it was Bentley himself who used the C int type, so it hardly seems
unreasonable to blame him.

The original program that he verified was in pseudocode equivalent to
the following (not tested) Python. The odd spec is due to Bentley using
1-based arrays. From the 1986 book Programming Pearls

def binsearch(x, t):
"If t is in sorted x[1:n], return its index; otherwise 0"
#
L,U = 1, len(x)-1
while True:
if L > U: return 0
m = (L+U)/2
if x[m] < t: L = m+1
elif x[m] == t: return m
elif x[m] > t: U = m-1

He then translated into an unspecified dialect of BASIC, but it is
consistent with Microsoft GW-BASIC. If so, L and U were float variables,
while the largest possible array size for x was 32767. So as near as I
can tell with that dialect, there was no possible problem with L+U
overflowing or wrapping. Other dialects, I am not sure.

So I revise my statement to "I consider it wrong to blame the Bentley
that wrote the original program" ;-).

If he later translated to C and fell into the residue class trap, then
that reinforces my contention that using residue classes as ints is
error prone.

Terry Jan Reedy

 

[John Nagle]

kj, as Piet van Oostrum as said, that's the difference between mutable
an immutable. It comes from the procedural nature of Python, and
probably an explanation of such topic can't be avoided if you want to
learn/teach Python.

The problem with Python's mutable/immutable distinction is that
it's not very visible. In a language with no declarations, no named
constants, and no parameter attributes like "value", "in", "out", or
"const", it's not at all obvious which functions can modify what.
Which is usually the place where this causes a problem.

The classic, of course, is

def additemtolist(item, lst = []) :
lst.append(item)
return(lst)

lista = additemtolist(1)
listb = additemtolist(2)
print(listb)

The general problem is inherent in Python's design. This particular problem,
though, results in the occasional suggestion that parameters shouldn't
be allowed to have mutable defaults.

John Nagle

 

[Piet van Oostrum]

IV> But it was Bentley himself who used the C int type, so it hardly seems
IV> unreasonable to blame him.

If you are on a 32-bit machine, and the array to be searched contains
ints, floats or doubles, the the array must be < 2^32 bytes in size, and
as each element is at least 4 bytes, the indices are less than 2^30, so
l+u < 2^31. Therefore there is no overflow at all. I think the Bentley
programs were formulated in terms of arrays of ints. So his
implementations were safe.

If you are on a 64-bit machine you shouldn't use int for the indices
anyway (supposing int is 32 bits) but longs and then the same reasoning
shows that there are no overflows. Only when you have an array of shorts
or bytes (chars) you get the problem.

In that case the alternative formulation l + (u-l)/2 is more
robust and therefore preferable.

 

[Hendrik van Rooyen]

I must admit, it never crossed my mind that anyone here would claim that
there was no creativity involved in programming, that it was all a
mindless, algorithmic process capable of being done by a simple
mechanical device.

"Programming" is the step of going from the "design" to something
that tells the machine how to implement the design.

The creativity could, arguably, be in the "Design".
Not in the translation to python, or assembler.
No way. That is just coding.

This is certainly the accusation made against *bad* programmers -- that
they can't actually solve new, unique problems, but just apply recipes
they learned without any insight or intelligence. The sort of people who
program so poorly that "a trained monkey could do what they do".

Do you really think that applies to good programmers too? If so, then a
good code generator should be able to replace any programmer. Is that
what you believe?

Should eventually be possible, with sufficient restrictions to start off.
UML wants to go this route...

But may my eyes be stopped and my bones be heaped with dust
ere I see the day...

>

Did I say that?

No. I just read it like that to irritate you.

Chefs are authorities on OTHER HUMAN ACTIVITIES.




Somebody should teach Hendrik that human beings have been creating TOOLS
for hundreds of thousands of years. People have been creating tools to
build tools for thousands of years. Software is just more of the same.

I disagree - I actually own some machine tools, so I am a little
bit acquainted with what they can do, and it is not at all like computing
at any level I can think of - they are merely extensions of the hand, making
the transformation of materials more accurate and faster.

The line only becomes blurred when a processor is added, and a STORED
PROGRAM is brought into the equation.

Even *soup stock* fits the same profile as what Hendrik claims is almost
unique to programming. On its own, soup stock is totally useless. But you
make it, now, so you can you feed it into something else later on.

Or instant coffee.

No, Henrik, if that's the best you can do, it's not very good. It is
rather sad, but also hilarious, that the most different thing you have
noticed about software is that it's just like instant coffee.

You have a wonderful ability to grab hold of part of a definition
and to ignore the rest, just like I can misread what you write.

Coffee and soup stay coffee and soup on re hydration. Mixing it
in with something else is not at all the same - it does not "DO" anything
else in conjunction with the thing it is fed into - how is that like
programming, and executing a program?

I am sorry if you are confusing the drinking of coffee,
which is an ancilliary activity to programming, with the
actual programming itself.

This is a highly significant difference, IMHO.

[...]
He talks about how "when all is said and done, the only thing
computers can do for us is to manipulate symbols and produce results
of such manipulations" and he emphasises the "uninterpreted" nature of
mechanical symbol manipulation, i.e. that the machine is doing it
mindlessly.

"Manipulate symbols" is so abstract as to be pointless. By that
reasoning, I can build a "computer" consisting of a box open at the top.
I represent a symbol by an object (say, a helium-filled balloon, or a
stone), instead of a pattern of bits. I manipulate the symbol by holding
the object over the box and letting go. If it flies up into the sky,
that represents the symbol "Love is War", if it falls into the box, it
represents the symbol "Strength is Blue", and if it just floats there,
it represents "Cheddar Cheese". This is a deterministic, analog computer
which manipulates symbols. Great.

And utterly, utterly useless. So what is my computer lacking that real
computers have? When you have answered that question, you'll see why
Dijkstra's claim is under-specified.

So if computers do not manipulate symbols, what is it that they do?

Did I say they don't manipulate symbols?

No you wanted someone to tell you how to make your
box machine useful, and that was too difficult, so I went this way.

They can't reason? Then what are they doing when they manipulate symbols?

They simply manipulate symbols.
They really do.
There is no reasoning involved.

Any reasoning that is done, was done in the mind of the human who designed
the system, and the the machine simply manipulates the implementation of
the abstract symbols, following the implementation of the abstract rules that
were laid down. No reasoning at run time at all.

Lots of decision making though - and it is this ability to do this now, and
something else later, that tricks the casual observer into thinking that there
is somebody at home - a reasoning ghost in the machine.

Yet again, it didn't even cross my mind that somebody would make this
claim. My entire point is that it's not enough to just "manipulate
symbols", you have to manipulate symbols the correct way, following laws
of logic, so that the computer can *mindlessly* reason.

No.

There is no requirement for dragging in things like "the laws of logic"
or any arbitrarily chosen subset. You can build a machine to do
essentially "anything" - and people like Turing and his ilk have
spent a lot of skull sweat to try to define what is "general purpose",
to enable you to do "anything"

If you're going to take that argument, then I'll remind you that there
are no symbols inside a computer. There are only bits. And in fact, there
aren't even any bits -- there are only analog voltages, and analog
magnetic fields.

Duh - sorry to hear that - I have only been doing digital electronics
now for more years than I care to remember - but maybe there
is a difference in how you define "analogue". - maybe something like:
"if I can measure it with a multimeter, it is an analogue signal, because
a multimeter is capable of measuring analogue signals" - a bit fallacious.

More seriously, I again differ on the symbol bit - I am, right now,
working on a little processor that mindlessly does I/O, by manipulating
bits from one representation to another. In this case, the symbols
and the bits are mostly identical - but please do not try to tell
me that there are no symbols inside the little processors'
memory - I know they are there, because I have arranged for
them to be put there, via an RS-232 feed.

And my stored program actually arranges for the incoming symbols
to do things like activating output relays, and changes on input lines
actually cause other symbols to be transmitted out of the RS-232
port. The whole thing is simply rotten with symbology - in fact all
it does, is manipulating the implementation of the abstract symbols
in my mind.
It does so mindlessly.
This specific thing is so simple, that it hardly uses the
"logical ability" of the processor. And please remember that
for a function with two input bits and a single output bit, there can
at most be eight possible outcomes, not all of which are useful, for
some definition of useful. But they exist, and you can use them, if
you want. And you do not even have to be consistent, if you do not
want to be, or if it is convenient not to be.

I think it is this horrendous freedom that Dijkstra was talking about
when he was referring to the "power beyond your wildest dreams",
or some such.

As I said above, it's not enough to just manipulate symbols. Here's a set
of rules to manipulate symbols:

X => 0

or in English, "Any symbol becomes the zero symbol".

That's symbol manipulation. Utterly useless. This is why it's not enough
to just manipulate symbols, you have to manipulate them THE RIGHT WAY.

No.
There is no RIGHT WAY.
Really.
There are only ways that are useful, or convenient.

In my little processor, I can cause any result
to occur, and the rules can be as silly as your
example - if it is useful for you, under some
circumstances, for all symbols to become the
symbol for zero, then go for it - The point is that
there is nothing prohibiting it to be adopted as a
rule for a machine to implement.

/dev/null anyone?

- Hendrik

 

[Hendrik van Rooyen]

I've always found cooking an apt metaphor for programming.

No this is wrong.

Writing a recipe or a cookbook is like programming.

Cooking, following a recipe, is like running a program.

- Hendrik

 

[Hendrik van Rooyen]

John O'Hagan wrote:

The drawings produced by an architect, the script of a play, the score of a

piece of music, and the draft of a piece of >legislation are all examples of
other things which are "useless" until they are interpreted in some way.

Granted.
But...

There are countless human activities which require a program, i.e. a conscious

plan or strategy, formed at least partly >by a creative process, and a computer
program is just a special case of this.

The difference is that for a piece of music, or a recipe for
"bobotie", there is room for artistry also in the performance
or preparation.

If the piece of music is reduced to a scroll with holes in it
and played on a pianola, then nobody in his right mind
would call the mechanically produced sounds
"a great performance".

And this is the essential difference that sets programming apart from
cookbook writing or drawing architectural plans - the one thing that
makes the real difference is the mindlessness of the performer.

(maybe I should conceed that writing legislation is a form of
programming, as the constabulary does not have a reputation
for anything other than a plodding consistency)

I use Python as a tool for writing music, but I find I need both logical

reasoning and creativity to do either. In fact, I >find programming very similar
to writing music in a rigorous contrapuntal style, where each set of choices
constrains >each other, and there is a deep aesthetic satisfaction in getting it
right.

Getting it right has to do with the design, not the programming -

Have you ever struggled to get something right, and then one day
you take a different tack, and suddenly it is as if you cannot do
anything wrong - everything just falls into place? - That is the time
that you get the good feeling.

The difference between the one and the other is the difference
between bad or indifferent design and good design. When you
have a good design, the rest follows. If your design is crud, no
matter what you do, you struggle and nothing comes out just
right, despite heroic effort.

Now this stuff is easy to talk about, and immensely difficult to
do - it takes experience, some skill, some cunning, and a
willingness to experiment in an egoless fashion, amongst other
things.

And then the stupid compiler completely screws up your intent...


- Hendrik

 

[D'Arcy J.M. Cain]

"Programming" is the step of going from the "design" to something
that tells the machine how to implement the design.

The creativity could, arguably, be in the "Design".
Not in the translation to python, or assembler.
No way. That is just coding.

One might also argue that divorcing the design from the code is the
problem in a lot of legacy code. See Agile Programming methods. Now
you could say that there is a design step still in talking to the
client and making a plan in your head or in some notes but that's like
saying that Michelangelo was done creating after discussing the Sistine
Chapel with Pope Sixtus and that the rest was just a house painting job.

 

[Hendrik van Rooyen]

One might also argue that divorcing the design from the code is the
problem in a lot of legacy code. See Agile Programming methods. Now
you could say that there is a design step still in talking to the
client and making a plan in your head or in some notes but that's like
saying that Michelangelo was done creating after discussing the Sistine
Chapel with Pope Sixtus and that the rest was just a house painting job.

How do you know that it was not exactly like that - he did, after all, take
a much longer time than expected to complete the job - just like a house
painter that gets paid by the hour.

It is also unreasonable to assume the opposite fallacy - that he was in
a creative frenzy from the start to the time at the end when he was
cleaning his brush after applying the last spot of paint.

But it is a valid point - it is often difficult to draw the line between the
design and the implementation - and one of the reasons that we all
like to program in python, is that it is almost a language that is a
design language that can also be run directly. - I have lately been doing
stuff like writing rough prototypes using python syntax to serve as
designs for some of the assembler thingies I do. If you muck around
a bit at the lower level, you will also be more aware of the dichotomy
between the design and the implementation - in python, it is not obvious
at all. In assembler, it is glaring. But in either place, if you get it wrong,
you suffer. - your programs cripple along, or they hardly do what
you thought they would, and they bear no relationship with what the
customer wanted.

- Hendrik

 

[greg]

The creativity could, arguably, be in the "Design".
Not in the translation to python, or assembler.
No way. That is just coding.

No, the mechanical part of the process is called compiling,
and we have programs to do it for us.

By the time you've specified the design so rigorously
that not the slightest spark of creativity is needed
to implement it, you *have* coded it.

 

[Calroc]

On Jul 9, 1:20 pm, Steven D'Aprano <st...@REMOVE-THIS-
cybersource.com.au> wrote:
[...]

You'll excuse my skepticism about all these claims about how anyone can
program, how easy it is to teach the fundamentals of Turing Machines and
functional programming to anybody at all. Prove it. Where are your peer-
reviewed studies demonstrating such successes on randomly chosen people,
not self-selected motivated, higher-than-average intelligence students?

I'm engaged presently in starting a school to teach programming from
the ground up, based roughly on the curriculum outlined in the article
I mentioned. I can't randomly select students but I do intend to
gather data about who does how well from what starting conditions.

I'm excited about formal methods because one, I just heard about them,
and two, they provide me with a much more well-fleshed-out way to
bridge rigorously from "raw" Turing machine models to higher order
abstractions.

I'm confident that anyone who can play Sudoku can learn programming
and formal methods.

In the real world, human beings are prone to serious cognitive biases and
errors. Our brains are buggy. Take any list of reasoning fallacies, and
you'll find the majority of people have difficulty avoid them. The first
struggle is to get them to even accept that they *are* fallacies, but
even once they have intellectually accepted it, getting them to live up
to that knowledge in practice is much, much harder.

In fact I'd go further and say that *every single person*, no matter how
intelligent and well-educated, will fall for cognitive biases and
fallacious reasoning on a regular basis.

I agree completely. One of my chief goals is to "debug" human
reasoning to whatever extent possible. This is precisely where I
expect training in computer programming to come in handy. The machine
symbol manipulator is not going to be fooled by reasoning fallacies.
Fluency in rigorous symbol manipulation can only help us cope with the
vagaries of our too-often sub-rational wetware.

I think the real win starts when computers can be used as a
communication medium, not for blogs and tweets and SMS txt and IM and
VoIP, but for reasoned symbolically coded discussion.

In practice? In principle? Programming in principle is not the same as it
is performed in practice.

But in either case, programming requires both the logical reasoning of
mathematics and the creativity of the arts. Funnily enough,
mathematicians will tell you that mathematics requires the same, and so
will the best artists. I think mathematicians, engineers, artists, even
great chefs, will pour scorn on your claim that programming is not like
any other human activity.

Well it's actually Dijkstra's claim, and I find it reasonable, that
programming has two novel or unique aspects not present in other areas
of human endeavor: vast scale and digital mechanism.

http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html

[...]

He talks about how "when all is said and done, the only thing computers
can do for us is to manipulate symbols and produce results of such
manipulations" and he emphasises the "uninterpreted" nature of
mechanical symbol manipulation, i.e. that the machine is doing it
mindlessly.

"Manipulate symbols" is so abstract as to be pointless. By that

That's the "koan form", longhand he means the Boolean domain {true,
false}, the logical operations and their algebraic relationships, and
the means of using same to deduce new formulae.

reasoning, I can build a "computer" consisting of a box open at the top.
I represent a symbol by an object (say, a helium-filled balloon, or a
stone), instead of a pattern of bits. I manipulate the symbol by holding
the object over the box and letting go. If it flies up into the sky, that
represents the symbol "Love is War", if it falls into the box, it
represents the symbol "Strength is Blue", and if it just floats there, it
represents "Cheddar Cheese". This is a deterministic, analog computer
which manipulates symbols. Great.

And utterly, utterly useless. So what is my computer lacking that real
computers have? When you have answered that question, you'll see why
Dijkstra's claim is under-specified.

Well, you said it yourself: your computer is lacking utility.


[...]

What is an uninterpreted formula? If you don't interpret it, how can you
distinguish it from random noise?

Uninterpreted formula means that you manipulate the symbols without
thinking about what they mean. You just use the rules on the formulae
as such. To be useful, once you're "done" with them you can consider
their meaning. You can distinguish it at any time, but Dijktra's
saying that we should pay attention to the [mathematical, logical]
reasoning process as it's own thing, without reference to the meaning
of the symbols, at least temporarily.


[...]

What nonsense. The keys to the kingdom are the abstractions.

Here's an exercise for you, if you dare. It's not that difficult to
remove the abstraction from integer addition, to explain it in terms of
bit manipulation. If you prefer, you can write a Turing Machine instead.

Now try doing the same thing for Quicksort. Don't worry, we'll wait.

Once you've done that, let's see you implement a practical, scalable, non-
toy webserver as a Turing Machine.

No, it's not the fundamental operations that open the doors to the
kingdom. It's the abstractions. The history of computing is to gain more
and more power by leveraging better and better abstractions.

I agree that "better and better abstractions" are the key(s), but I
strongly disagree that the fundamental operations are not, uh, key to
those keys.

There are two intertwined phenomenon:

1) formulae, written in symbols

2) deriving new formulae by applying [in]formal methods to existing
formulae

The rules, and the application of those rules, are two separate but
compatible phenomenon. (Compatible in that you can encode the latter
in terms of the former. This is the essential "trick" of mechanized
thought.)

Now (1) is constantly being elaborated, these elaborations are the
"higher" abstractions we're talking about.

But (2) stays the same(-ish) no matter how high you go, and (2) is the
process by which all the higher (1)'s come from, so if we get it right
(and by right I mean of course by using rigorous proofs, formal
methods et. al.) from the get go and keep it right, we're golden.

I do literally intend to teach e.g. "integer addition ... in terms of
bit manipulation" and a bit of parsing too. But I intend to rapidly
bring students to a Forth or Forth-like stage, and then immediately
create simple parsers that implement, for example, C for loops, and
other "higher" abstractions.

Highly abridged, this is the curriculum: Enough about bits to bring
them to bytes, enough bytes to bring them to RAM, enough RAM to
implement a crude CPU, enough CPU to implement a bit of Forth, enough
Forth to implement parsers, and enough parsing (and compilation and
interpreting, etc.) to let them grok languages in general.

Formal methods gives me a wide straight road from each stage to the
next.

[...]

Quoting Dijkstra again [1]: "Before we part, I would like to invite you
to consider the following way of doing justice to computing's radical
novelty in an introductory programming course.

"On the one hand, we teach what looks like the predicate calculus, but
we do it very differently from the philosophers. In order to train the
novice programmer in the manipulation of uninterpreted formulae, we
teach it more as boolean algebra, familiarizing the student with all
algebraic properties of the logical connectives. To further sever the
links to intuition, we rename the values {true, false} of the boolean
domain as {black, white}.

This is supposed to be a good thing?

Oh my. It must be nice in that ivory tower, never having to deal with
anyone who hasn't already been winnowed by years of study and self-
selection before taking on a comp sci course.

I don't think Dijkstra would have taken that suggestion seriously if he
had to teach school kids instead of college adults.

I'm not going to teach it exactly like he outlines there, but I really
am going to try the curriculum I outlined. I'll post videos. :]

...


No. What I thought was, how the hell are you supposed to manipulate
symbols without a language to describe what sort of manipulations you can
do?

Direct-manipulation graphical Abstract Syntax Trees.



[...]

I shall manfully resist the urge to make sarcastic comments about
ignorant PHP developers, and instead refer you to my earlier reply to you
about cognitive biases. For extra points, can you identify all the
fallacious reasoning in that paragraph of yours?

I'll pass. I should have resisted the urge to whinge about him in the
first place.

But those abstractions just get in the way, according to you. He should
be programming in the bare metal, doing pure symbol manipulation without
language.

No, the abstractions are useful, but their utility is tied to their
reliability, which in turn derives from the formal rigour of the
proofs of the abstractions' correctness.

My issues with modern art are, that too many of these abstractions are
not /proven/, and they are both frozen and fractured by the existing
milieu of "static" mutually incompatible programming languages.

I see a possibility for something better.

If programming is symbol manipulation, then you should remember that the
user interface is also symbol manipulation, and it is a MUCH harder
problem than databases, sorting, searching, and all the other problems
you learn about in academia. The user interface has to communicate over a
rich but noisy channel using multiple under-specified protocols to a
couple of pounds of meat which processes information using buggy
heuristics evolved over millions of years to find the ripe fruit, avoid
being eaten, and have sex. If you think getting XML was hard, that's
*nothing* compared to user interfaces.

The fact that even bad UIs work at all is a credit to the heuristics,
bugs and all, in the meat.

Ok, yes, but have you read Jef Raskin's "the Humane Interface"?

Sorry. I can't believe that I was so melodramatic.

And the secret of getting rich on the stock market is to buy low, sell
high. Very true, and very pointless. How do you derive the formula
correctly?

Do you have an algorithm to do so? If so, how do you know that algorithm
is correct?

Well we know logic works, we can trust that. The algorithm of proving
the formula is logic.

That's impossible. Not just impractical, or hard, or subject to hardware
failures, but impossible.

I really shouldn't need to raise this to anyone with pretensions of being
a Computer Scientist and not just a programmer, but... try proving an
arbitrary program will *halt*.

If you can't do that, then what makes you think you can prove all useful,
necessary programs are correct?

It may well be that there are useful, necessary programs that are
impossible to prove correct. I'm not trying to claim there aren't
such.

I think that wherever that's not the case, wherever useful necessary
programs can be proven, they should be.

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.

Just because it's unattainable doesn't make it undesirable. And who
knows? Maybe the horse will learn to sing.

Again with Dijkstra[3]: "The prime paradigma of the pragmatic designer
is known as "poor man's induction", i.e. he believes in his design as
long as "it works", i.e. until faced with evidence to the contrary. (He
will then "fix the design".)

Yes, that is the only way it can be.

The scientific designer, however, believes
in his design because he understands why it will work under all
circumstances.

Really? Under *all* circumstances?

Memory failures? Stray cosmic radiation flipping bits? Noise in the power
supply?

What's that you say? "That's cheating, the software designer can't be
expected to deal with the actual reality of computers!!! We work in an
abstract realm where computers never run out of memory, swapping never
occurs, and the floating point unit is always correct!"

First, yes, that could be considered cheating. We don't expect
automotive engineers to design for resistance to meteor strikes.
Second, those issues plague all programs, formally derived or not.
Formal methods certainly can't hurt. Third, in cases where you do
want reliability in the face of things like cosmic rays you're going
to want to use formal methods to achieve it.

And last but not least, it may be possible to "parameterize" the
abstractions we derive with information about their susceptibility to
stability of their underlying abstractions.

Fail enough. I don't want to make it too hard for you.

Okay, so let's compare the mere "pragmatic designer" with his provisional
expectation that his code is correct, and Dijkstra's "scientific
designer". He understands his code is correct. Wonderful!

Er, *how exactly* does he reach that understanding?

He reasons about the logic of the program. Great! I can do that. See,
here's a proof that binary search is correct. How easy this is.

Now try it for some non-trivial piece of code. Say, the Linux kernel.
This may take a while...

Well, I'd start with Minix 3... But really the method would be to
build up provably correct compounds out of proven sub-assemblies.
Even if it takes a long time is it time wasted? A provably correct OS
is kind of a neat idea IMO.

What guarantee do we have that the scientific designer's reasoning was
correct? I mean, sure he is convinced he has reasoned correctly, but he
would, wouldn't he? If he was unsure, he'd keep reasoning (or ask for
help), until he was sure. But being sure doesn't make him correct. It
just makes him sure.

So how do you verify the verification?

Peer review and run it through a mechanical verifier. There is a self-
reflexive loop there but it's not infinite. If it was we couldn't
implement any computer.

And speaking of binary search:

[Bentley's binary search bug]

This is a perfect example of leaky abstraction. The C "integer"
doesn't behave like a "real" integer but part of the algorithm's
implementation relied on the tacit overlap between C ints and integers
up to a certain value. This is the sort of thing that could be
annotated onto the symbolic representation of the algorithm and used
to compile provably correct machine code (for various platforms.)

If the same proven algorithm had been implemented on top of a correct
integer abstraction (like python's long int) it wouldn't have had that
bug.

(And yes, there would still be limits, truly vast arrays could
conceivably result in memory exhaustion during execution of the sort.
I think the answer there lies in being able to represent or calculate
the limits of an algorithm explicitly, the better to use it correctly
in other code.)

Perhaps the "scientific designer" should be a little less arrogant, and
take note of the lesson of real science: all knowledge is provisional and
subject to correction and falsification.

(I apologize for my arrogance on behalf of formal methods, I just
found out about them and I'm all giddy and irritating.)

Which really makes the "scientific designer" just a slightly more clever
and effective "pragmatic designer", doesn't it?

Um, er, well, scientists are ultimate pragmatists, and Dijkstra's
description of "pragmatic designer" above could well be applied to
"scientific designers". The difference turns on /why/ each person has
confidence is his design: one can prove mathematically that his design
is correct while the other is ... sure.

Whether or not the delivered software is actually flawless, the
difference seems to me more than just "slightly more clever and
effective".

Given Dijkstra's definition of "scientific design", it certainly would.
It would be as drastic a change as the discovery of Immovable Objects and
Irresistible Forces would be to engineering, or the invention of a
Universal Solvent for chemistry, or any other impossibility.


It's not a matter of preferring no obvious errors, as understanding the
limitations of reality. You simply can't do better than no obvious errors
(although of course you can do worse) -- the only question is what you
call "obvious".

It may be expensive, it may be difficult, and it may certainly be
impossible, but I feel the shift from ad hoc software creation to
rigorous scientific software production is obvious. To me it's like
the shift from astrology to astronomy, or from alchemy to chemistry.


~Simon

 

[Paul Rubin]

I'm engaged presently in starting a school to teach programming from
the ground up, based roughly on the curriculum outlined in the article
I mentioned. ...
I'm excited about formal methods because one, I just heard about them,

Formal methods are a big and complicated subject. Right after you
heard about them is probably not the best time to start teaching them.
Better get to understand them yourself first.

 

[greg]

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.

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.

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!

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.

 

[Simon Forman]

Formal methods are a big and complicated subject. Right after you
heard about them is probably not the best time to start teaching them.
Better get to understand them yourself first.

Very good point.

But I'm glad it's there to study, these are wheels I don't have to
invent for myself.

~Simon

 

[Simon Forman]

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.

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

 

[Paul Rubin]

But I'm glad it's there to study, these are wheels I don't have to
invent for myself.

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

might be an interesting place to start.