Tracing the evolution of formal methods from Hoare to today, this talk suggests ways to teach program reasoning to all programmers.
Speaker
Carroll Morgan
Agenda
11:00am - Talk
12:00pm - Questions and answers
1:00pm - Event closes
Synopsis
Formal Methods (for computing) was enabled by Hoare's “An axiomatic basis for computer programming” in 1969, where Formal meant “in the sense of formal logic”, i.e. reasoning based on manipulation of symbols which themselves had no intrinsic meaning (in the sense of Hilbert).
Hoare's paper had itself been enabled by Floyd's “Assigning meanings to programs” just two years earlier, whose informal message might well have been -- in retrospect at least -- “Don't write your comments inside a flowchart's boxes: instead, write them on the lines connecting those boxes.”
After that however, Formal Methods gradually became “Use preconditions, postconditions, invariants, all written in predicate logic over your program's variables.” to improve the chance that your program does what it's supposed to do, and even “Use the very formality of that logic, and its own calculus even if by hand, to help you do that.” Even better, “Use that formality to help you develop your program, your algorithm: strive for correctness by construction.”
And so, more than fifty years later, it's that very formality that has made it possible to verify extremely complicated programs, even whole operating systems, by using computer-implemented proof tools: for “formality” is all those tools understand. Yet over all those decades the quality of code produced by the average programmer might not have improved much at all.
In this talk I will present some ideas for fixing that, targetting in particular the “average programmer”. I'll make suggestions about when we might introduce students to reasoning about programs, how to do that introduction, and what kind of assessment might work for many hundreds of submissions of exercises, quizzes and exams that are too onerous at that scale to mark by hand.
About the speaker
Carroll Morgan obtained a BSc at the University of New South Wales and a PhD at the University of Sydney. He then worked in industry for about 3 years, a programmer/analyst at a small company in Sydney.
In 1982 he moved to the UK to join Tony Hoare's Programming Research Group, first as a post-doctoral researcher at Wolfson College, then in 1985 taking up a permanent Fellowship in Computation at Oxford (Pembroke College). When he returned to Australia in 2000 he first worked again in industry (J2EE-based web front-ends), but soon (re-)joined UNSW, collaborating as an adjunct professor with Ken Robinson.
In 2002, about to lead the Formal Methods Group within the newly formed NICTA, he was at the same time awarded a five-year Australian Professorial Fellowship at UNSW to start in 2003. Taking the latter, he remained at UNSW from then on, within NICTA that became Data61 that in turn became the Trustworthy Systems group, which is now led by Gernot Heiser.
He's authored (in some cases jointly) the texts "Programming from Specifications", "Abstraction, Refinement and Proof for Probabilistic Systems" with Annabelle McIver, "The Science of Quantitative Information Flow" with Mário Alvim, Konstantinos Chatzikokolakis , Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith and, most recently, the topic of this talk "Formal Methods, Informally: How to write programs that work". In 2015 he was awarded (with the other five authors above) the NSA's Best Scientific Cybersecurity Paper award.
He became Professor Emeritus at UNSW upon his retirement in 2024, and remains a member of Trustworthy Systems there.
Our events are for adults aged 16 years and over.
This meeting is conducted in accordance with the BCS Code of Conduct for Meetings.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
Please note, if you have any accessibility needs, please let us know via groups@bcs.uk, and we’ll work with you to make suitable arrangements.
BCS privacy notice: your data will be processed by BCS in accordance with our data privacy notice.
Photography: by attending this event, you may be photographed or filmed. Please speak to a member of staff if you do not wish to be included.
This event is brought to you by: FACS (Formal Aspects of Computing Science) group
