Banquet Speech at ZUM95
Limerick, Ireland
7 September 1995

David Gries

Computer Science
Cornell University
Ithaca, NY 14853

Abstract

The World is turning to C,
Though at best it is taught awkwardly.
But we don't have to mope,
There's a glimmer of hope,
In the methods of formality.


About the abstract (written 6 months after the abstract)

An abstract is written with speed
Long before the talk is in need.
Oft there's little relation
'Twixt abstract and oration.
If that's so, do forgive me I plead.


A limerick contest, I here,
Goes along with this conf'rence, three cheers!
Here's some thirty lim'ricks
To add to their picks
This will keep them all busy, I fear!


Introduction

The president Mary of Eire
Was supposed to come to regale ya.
But matters of state
Made her cancel the date,
So you're stuck with this guy from Bavaria!

[Bavaria, did he say Bavaria?]

Well, I got my degree in that place,
And my ancestors come from that race.
Though great New York C
Was the birthplace of me,
And CS at Cornell is my base.

So I don't have a real PhD.
It's the Dr. Rer. Nat. that's for me.
And it's from MIT
--On your side of the sea--
Munich Inst. of Technolology!

About this conference

This conf'rence is all about Z.
( oh me! Is that right? Let me see.
It's Zee or it's Zed
Oh my face will be red
If I said the wrong one, Oh oh me!

The Atlantic will help me decide,
For, thank goodness, it does have two sides.
Its West and its East
Rhyme with Zedst and with Zeest,
But negation of rhyme does decide.

Now, the Irish live on its East?
Yes, from New York I flew East on that beast.
In the West it's not Zedst,
So the East has it Zedst,
So it's Zed that I say at this feast.)

This conf'rence is all about Z.
Well, that's far too narrowly said.
It's formality
And its uses, you see,
From which we all earn our good bread.

Using formality

Now, how is formality used?
How is Z apparently used?
The main way it seems
Is to specify things
Like the programs or systems we choose.

Specifying is certainly great,
For it helps to disambiguate.
It can make something clean
And precise like a dream.
If all specified that would be great!

But specs are but part of the game!
It's reas'ning that's most of the gain.
With reas'ning we prove,
Analyze, and review,
The programs we have to explain.

Whenever a field gets complex,
It turns to the math for a fix.
Notations 're revealed
For concepts of the field
And reasoning rules are then sketched.

Reasoning rules are the keys,
For without them, we can't analyze.
Notations turn dumb,
Lethargic and numb,
When their rules are not utilized.

With programs, it's logic to which
We turn when complexities twitch.
But logics of old
Help less in this mold.
So it's certain that we have to switch.

For logic, I urge you to poke
Through a text that I recently wrote
with Freddie B. Schneider,
A masterful writer
Without whom the text were a joke.

Calculational logic have we,
With equivalence as a big key.
And it's taught, to our joy,
As a tool to employ,
Not only a thing to study.

With a skill in this logic, we're sure
We can reason 'bout programs and more.
We can form pretty specs,
Analyze all aspects;
And our faith is in logic restored.

(Whew,

At last I managed to do
What I came to Lim'rick to do.
A little advert
For our text cannot hurt.
And it helps Springer's bank account, too.)

On Simplicity

One topic I feel I must broach
Is Simplicity as a good coach.
It was Einstein who penned,
``Make it simple, my friend,
But no simpler than it can be coaxed.

[Aside: Einstein said ``Make everything as simple as possible, but no simpler.'' This was the best I could do to limerick it. Ha.]

Simplicity really is key
When it comes to formality.
In making a choice
Let't have a strong voice,
And then it will do its duty.

A little example

I'll give you a case, if I may,
Where simplicity saves us the day.
It's the undefined
that clutters our mind,
So we'll see how to deal it away.

Suppose we have bot[tom], false, and true,
A three-valued logic to you.
But then I can show
That properties go,
So the proofs are much harder to do.

Assoc. of equiv. is no more.
Excluded middle feels sore.
And other props, too,
Get complex and soo,
The logic is property poor!

So--

For simplicity's sake we are sold
On the 2-valued logic of old.
For our simple mind,
The big undefined
Is banished from logic, we're told.

So what's one divided by nought?
An answer to that must be sought.
It's not undefined,
Which is out of our mind;
A real value is one div by nought.

What value is it, you ask me?
Well, you won't get the answer from me.
It's not specified!
No-one dotted the eye!
It's a value that you cannot see.

When a function f is explained,
It's defined on all its domain.
But for argument b,
Perhaps we can't see
What f of b actually attained.

Underspec is the name of the game
That adds to simplicity's fame.
Partial functions are gone!
Only totals are on!
Underspecified totals remain.

Now, underspec simplifies Z,
Which has too many arrows, it's said.
Almost half of them go
With partials and so,
There's much less to deal with in Z.

Underspec has the nice quality
That it mimics informality.
...
Can't explain what I mean
In a limerick clean,
So on this you just have to trust me!

A second example

There's notation I long ago met,
But haven't digested it yet.
You take a flaw chart,
Put rocks on its heart,
And call it a petrified net

Well, it's Petri net they tell me,
For its father is Mr. Petri,
But its math is not nice,
More complex than I likes!
So the petri net petrifies me!

I don't mean to hurt friend Petri.
And his net has good uses, agreed?
But as a good spec
Of a program --nyet!
For it's too operational, see?

So you see that goal Simplicity
Helps us all so semantically.
And syntax does, too,
get a lot cleaner through,
the striving for simplicity.

In closing

Well, I think I had better step down
Before you throw rocks at my crown.
My thanks, everyone
For a week of great fun.
In this wonderful little old town.