pith. sign in

arxiv: 1906.11425 · v1 · pith:BOCBFBROnew · submitted 2019-06-27 · 💻 cs.PL · cs.LO

Introducing Certified Compilation in Education by a Functional Language Approach

Per Lindgren (Lule{\aa} University of Technology) , Marcus Lindner (Lule{\aa} University of Technology) , Nils Fitinghoff (Lule{\aa} University of Technology) This is my paper

Pith reviewed 2026-05-25 14:18 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords certified compilationcompiler constructionWhy3formal methods educationverified compilerfunctional programmingcourse design
0
0 comments X

The pith

Certified compilation can be taught in introductory compiler courses to students without formal methods experience by using automated proofs in Why3.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper reports on the introduction of certified compilation techniques into an introductory course on Compiler Construction. It employs a functional language approach and relies on the Why3 framework to automate the proof process. This allows the teaching of logic, semantic modelling, and proofs through exercises that lead to students creating a formally verified compiler for a simple imperative language. The work includes details on course design, tool choice, teaching methods, and feedback from both students and instructors.

Core claim

Targeting students with little or no experience in formal methods, the proof process is highly automated using the Why3 framework. Underlying logic, semantic modelling and proofs are introduced along with exercises and assignments leading up to a formally verified compiler for a simplistic imperative language.

What carries the argument

The Why3 framework, which automates the proof process for semantic models written in a functional style.

If this is right

  • Students without formal methods background can complete exercises on logic and proofs.
  • Course assignments result in a formally verified compiler for a simplistic imperative language.
  • The integration combines compiler technology with certified compilation in one introductory class.
  • Evaluations provide insights into student and teacher perspectives on the method.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar automated tools could enable early introduction of verification in other CS courses like software engineering.
  • Adoption might require assessing how the functional approach aligns with students' existing programming knowledge.
  • Longer term, this could influence curricula to include certified compilation as standard in compiler classes.

Load-bearing premise

That students with little or no prior formal methods experience can successfully complete the semantic modelling and proof exercises using Why3 within the constraints of an introductory compiler course.

What would settle it

Student performance data showing that the majority cannot finish the proof-based assignments or produce the verified compiler would indicate the approach does not work as intended for the target audience.

read the original abstract

Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified compilation techniques through a functional language approach in an introductory course on Compiler Construction. Targeting students with little or no experience in formal methods, the proof process is highly automated using the Why3 framework. Underlying logic, semantic modelling and proofs are introduced along with exercises and assignments leading up to a formally verified compiler for a simplistic imperative language. This paper covers the motivation, course design, tool selection, and teaching methods, together with evaluations and suggested improvements from the perspectives of both students and teachers.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper describes the integration of certified compilation techniques into an introductory compiler construction course using the Why3 framework. Aimed at students with little formal methods experience, the course introduces logic, semantic modeling, and proofs through exercises and assignments, culminating in a formally verified compiler for a simplistic imperative language. It also discusses motivation, course design, tool selection, teaching methods, and evaluations from students and teachers.

Significance. If the approach proves effective for novices, this work could offer a practical template for embedding formal verification into standard CS compiler courses, potentially broadening access to certified compilation education.

major comments (1)
  1. [Evaluations] The abstract states that evaluations from students and teachers were collected, but the manuscript provides no details on survey methods, response rates, or specific outcomes (quantitative or qualitative). This leaves the central claim—that students with little or no formal-methods experience can complete semantic modelling and automated proofs in Why3—without observable supporting evidence.
minor comments (2)
  1. The description of the target imperative language and the exact scope of the verified compiler (supported features, size of the development) could be stated more explicitly in the introduction or course-design section to allow replication.
  2. Adding citations to prior educational uses of Why3 or other tools for teaching certified compilation would strengthen the related-work context.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for highlighting the lack of detail on evaluations. We agree this is a gap in the current manuscript and will address it directly in revision.

read point-by-point responses

  1. Referee: [Evaluations] The abstract states that evaluations from students and teachers were collected, but the manuscript provides no details on survey methods, response rates, or specific outcomes (quantitative or qualitative). This leaves the central claim—that students with little or no formal-methods experience can complete semantic modelling and automated proofs in Why3—without observable supporting evidence.

    Authors: We agree that the manuscript as submitted does not provide the requested details on the evaluation process, which weakens the evidential support for the central claim. In the revised manuscript we will add a new subsection (likely under Section 5 or a dedicated evaluation section) that reports: (1) survey methods (anonymous end-of-course questionnaires plus informal teacher debriefs), (2) response rates (e.g., number of student respondents out of total enrollment), and (3) concrete outcomes, including both quantitative results (average Likert-scale ratings on perceived difficulty of semantic modeling and proof automation) and selected qualitative student/teacher comments. These additions will make the supporting evidence observable while remaining faithful to the data actually collected. revision: yes

Circularity Check

0 steps flagged

No circularity: descriptive educational report with no derivations or predictions

full rationale

The paper is a descriptive report on course design for introducing certified compilation using Why3 in an introductory compiler course. It covers motivation, tool selection, teaching methods, exercises, and qualitative evaluations without any mathematical derivations, equations, fitted parameters, predictions, or uniqueness theorems. No load-bearing steps reduce to self-definition, self-citation chains, or fitted inputs by construction; the content is self-contained as an educational case study.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is an educational case study report and introduces no free parameters, mathematical axioms, or invented entities.

pith-pipeline@v0.9.0 · 5659 in / 1097 out tokens · 42516 ms · 2026-05-25T14:18:53.252308+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

9 extracted references · 9 canonical work pages

  1. [1]

    Aho, Monica S

    Alfred V. Aho, Monica S. Lam, Ravi Sethi & Jeffrey D. Ullman (2006): Compilers: Principles, Techniques, and Tools (2Nd Edition) . Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA

    work page 2006

  2. [2]

    In: Journées Francophones des Langages Applicatifs , Val d’Ajol, France, pp

    Martin Clochard & Léon Gondelman (2015): Double WP : Vers une preuve automatique d’un compi- lateur. In: Journées Francophones des Langages Applicatifs , Val d’Ajol, France, pp. 1–18. A vailable at https://hal.inria.fr/hal-01094488

    work page 2015

  3. [3]

    http://toccata.lri.fr/gallery/register_allocation.en.html

    Jean-Christophe Filliâtre & Martin Clochard (2013): A tiny register allocator for tree expres- sions. http://toccata.lri.fr/gallery/register_allocation.en.html. Online; accessed May 15th 2018

    work page 2013

  4. [4]

    Sabine Glesner, Simone Forster & Matthias Jäger (2005): A Program Result Checker for the Lexical Analysis of the GNU C Compiler . Electr. Notes Theor. Comput. Sci. 132(1), pp. 19–35, doi: 10.1016/ j.entcs.2005.01.029

    work page 2005

  5. [5]

    http://toccata.lri.fr/gallery/ double_wp.en.html

    Léon Gondelman & Martin Clochard (2013): Double WP . http://toccata.lri.fr/gallery/ double_wp.en.html. Online; accessed May 15th 2018

    work page 2013

  6. [6]

    O’Reilly Media, Inc

    Jason Hickey, Anil Madhavapeddy & Yaron Minsky (2014): Real World OCaml . "O’Reilly Media, Inc.". A vailable at http://www.worldcat.org/isbn/144932391

    work page arXiv 2014

  7. [7]

    http://why3.lri.fr/

    Inria (2013): Why3 - Home . http://why3.lri.fr/. Online; accessed May 15th 2018

    work page 2013

  8. [8]

    Communications of the ACM 52(7), pp

    Xavier Leroy (2009): Formal verification of a realistic compiler . Communications of the ACM 52(7), pp. 107–115, doi: 10.1145/1538788.1538814. A vailable at http://gallium.inria.fr/~xleroy/ publi/compcert-CACM.pdf

    work page doi:10.1145/1538788.1538814 2009

  9. [9]

    Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin & S teve Zdancewic (2012): Formalizing the LL VM intermediate representation for verified program tran sformations. In John Field & Michael Hicks, editors: POPL, ACM, pp. 427–440, doi: 10.1145/2103656.2103709. A vailable at http:// dblp.uni-trier.de/db/conf/popl/popl2012.html#ZhaoNMZ12

    work page doi:10.1145/2103656.2103709 2012