Why might we teach "Formal Methods" informally? And to whom? And when? Carroll Morgan

 BCS-FACS Online SeminarDate and time

Thursday 25 June, 11:00 am - 1:00 pm
Location

Online
Free registration
<https://www.bcs.org/events-calendar/2026/june/hybrid-why-might-we-teach-formal-methods-informally-and-to-whom-and-when/>

Note that this event is online only.

Timetable

11:00 am - Talk
12:00 pm - Questions and answers
1:00 pm - Event closes

Seminar Details

Title: Why might we teach "Formal Methods" informally? And to whom? And
when?

Speaker: Carroll Morgan

Abstract: 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.

*Biography*: 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.
This event is brought to you by: BCS-FACS Specialist Group - Formal Aspects
of Computing Science
<https://www.bcs.org/membership-and-registrations/member-communities/facs-formal-aspects-of-computing-science-group/>

 

" Charles Carroll Morgan (born 1952) is an American/Australian computer scientist who moved from the US to Australia in his early teens. He completed his education there (high school, university, several years in industry), including a Doctor of Philosophy (Ph.D.) degree from the University of Sydney, and then moved to the United Kingdom in the early 1980s. In 2000, he returned to Australia.

During the 1980s and 1990s, Morgan was based at the Oxford University Computing Laboratory in England as a researcher and lecturer working in the area of formal methods, and was a Fellow of Pembroke College. Having been influenced by the Z notation of Jean-Raymond Abrial, he authored Programming from Specifications as an attempt to combine the high-level specification aspects of Z, with the rigorous computer program derivation methods of Edsger W. Dijkstra. His treatment concentrated on elementary program constructs to make the material accessible to undergraduates in their early years.^[1] Some of the ideas there were later incorporated as elements of the B-Method by Abrial, when Abrial returned to Oxford in the last half of the 1980s."

https://en.wikipedia.org/wiki/Carroll_Morgan_(computer_scientist)