Notional Machines and Programming Language Semantics in Education

Motivation

A formal semantics of a language serves many purposes. It can help debug the language’s design, be used to prove type soundness, and guide optimizers to confirm that their work is correctness-preserving. In addition, it also serves as a comprehension tool. Semanticists assume that programmers can use a semantics to understand how a particular program will behave without being forced to resort to deconstructing the output from a black-box evaluator. Indeed, different semantic models vary in what aspects of program behavior they highlight and suppress.

Unfortunately, we know relatively little about how non-experts, such as students, actually employ a semantics. Which models are they able to grasp? How useful are these as they explain or debug programs? How does their use of models evolve with the kinds of programs they write? And does studying these kinds of questions yield any new insights into forms of semantics?

In contrast, formal semantics are evaluated by several criteria: full abstraction, adequacy, soundness and completeness, faithfulness to an underlying implementation, and so on. However, two dimensions have not been considered at all: utility to correcting misunderstandings, and usability by learners. Considering these will result in a better understanding of the role of semantics in learning. It will also identify and categorize semantic misunderstandings that learners suffer from. It may also result in insights that lead to new styles of semantics.

This Dagstuhl Seminar intends to bridge this gap. It will bring together representatives of the two communities—who usually travel in non-intersecting circles—to enable mutual understanding and cross-pollination. The programming languages community uses mathematics and focuses on formal results; the CER community uses social science methods and focuses on the impact on humans. Neither is superior: both are needed to arrive at a comprehensive solution to creating tools for learning.

The main aim of the seminar is to try to create a “notional machines” community by combining expertise in computing education and formal semantics. The seminar will educate each group on the methods and results of the other. It will then attempt to synthesize knowledge between the two, trying to identify solutions from semantics that aid education, and identify open problems.

Towards this aim, the seminar has several specific goals:

• Bring together key members of these different communities, with an eye towards people who are open-minded and receptive to the perspective of the other.
• Create tutorial sessions to educate participants on the existing knowledge, as well as methods, of each side.
• Enable Computing Education Research members to present open problems and look for solutions in semantics.
• Try to formulate interesting examples and test problems that can be used to evaluate results.