Banquet Speech at ZUM95 Limerick, Ireland 7 September 1995 David Gries Computer Science Cornell University Ithaca, NY 14853
AbstractThe 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!
IntroductionThe 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 conferenceThis 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 formalityNow, 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 SimplicityOne 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 exampleI'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 exampleThere'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 closingWell, 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.