Computer scienceDesign by ContractEulogyLanguage designMathematicsPersonalProgramming techniquesSoftware engineeringSoftware processSoftware verificationSoftware designTheoryWriting and styleHoare
Tony Hoare at the LASER summer school, September 2007 (All photographs in this article are by the author) Had they included just one of Tony Hoare’s major achievements, many scientific careers would be considered prestigious enough. His had a long list, which I am going to try to summarize, not pretending to get anywhere close ... Read more
It must be a sign of how terrified people are of Modern-AI, and running out of arguments to decry it, that we now read and hear, ever more often, pronouncements that “it is not intelligent”. They come from the many self-appointed great minds who pontificate about AI these days, as well as some truly great ... Read more
Société pour la Défense de l’Imparfait du Subjonctif (SDIS) Compte-rendu de l’assemblée annuelle 2025, 1er décembre 2025. Présents : Président, Secrétaire, Premier et Second vice-présidents, Trésorier, représentant des adhérents. Le Secrétaire (Bertrand Meyer) ouvre la séance à 17 heures et souhaite la bienvenue à tous les participants. La séance se poursuit avec le rapport du ... Read more
Computer scienceDesign by ContractEiffelFormal methods and proofsProgramming techniquesSoftware engineeringSoftware verificationSoftware designCloudflare
[This note was first published in my newsletter (23 November 2025. One can subscribe to the newsletter here.] I might sound like a broken record, but the CloudFlare outage is one more example of the consequences of the software industry making the wrong technical choices. Where were the contracts? Rust, by all accounts the language ... Read more
EducationEiffelEssayGeneral technologySoftware engineeringStandardizationWriting and styledefinitionstechnical definitions
(A version of this note was published as three separate articles in the Communications of the ACM blog.) Work in engineering, science or technology can only be effective if it relies on precisely defined concepts. For the fundamental notions taught at school, particularly in mathematics, physics, and chemistry, the definitions, honed over centuries, have become ... Read more
We are all familiar with the classical mode of teaching. The instructor and other attendees, each sitting alone in a geographical location as far away as possible from all the others, look at shared PowerPoint slide and a grid of black rectangles with names. The names refer to students, although they are usually not their ... Read more
Artificial IntelligenceEthicsGeneral technologyPolicyWriting and style
Here is an extract from of an exchange between ChatGPT and me. Previous elements: I am writing a text on a topic that I know well but not to the point of considering myself an expert. Along the way, I am asking ChatGPT for information, or confirmation of information that I think I know. Indeed, ... Read more
MathematicsSoftware engineeringWriting and styleExponentialExponentially
The news is so bad right now everywhere that it is natural to take refuge in discussing matters of (bad) style. I have things to say about the real issues too but not this time. I am following in the tradition of Niklaus Wirth who told me that he regularly sent letters of complaint to ... Read more
Artificial IntelligenceFormal methods and proofsProgramming techniquesPublication announcementSoftware engineeringSoftware processSoftware verificationSoftware designAutomatic Program RepairDebugging
New article: “Do AI models help produce verified bug fixes?” (Huang Li, Ilgiz Mustafin, Marco Piccioni, Alessandro Schena, Reto Weber and Bertrand Meyer), submitted for publication, preprint available on arXiv. Automatic Program Repair (APR) involves four steps: Locating the bug. Producing candidate corrections. Validating them (to make sure that they do correct the problem). Selecting the ... Read more
A Google search for something entirely unrelated led me to a very old issue of the Daily Nexus, the student newspaper of the University of California, Santa Barbara, where I was teaching back then. Apparently (I had forgotten all about it of course) I was piqued by a student’s letter to the editor, where he ... Read more
Computer scienceEducationEulogyFormal methods and proofsHistoryLanguage designMemoirProgramming techniquesPublication announcementSoftware engineering
Bertrand Meyer: Obituary for Niklaus Wirth, in Formal Aspects of Computing, volume 37, issue 2, pages 1-11, published 3 March 2025, available here (publisher’s site). Shortly after Niklaus Wirth — Turing Award winner for his many seminal contributions including Pascal, Algol W, Modula, virtual machines, Lilith/Ceres, railway diagrams, PL/360, seminal textbooks… — passed away last ... Read more
Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer and Yinling Liu, Lessons from Formally Verified Deployed Software Systems, submitted for publication (since March 2023), preprint available here for the full version (with detailed review of all 32 projects) and here for a shorter one (with same core content but only 11 detailed reviews, the others ... Read more
Computer scienceDesign by ContractEiffelFormal methods and proofsObject technologyPublication announcementRequirementsSoftware engineeringSoftware verificationTheory
Maria Naumcheva, Sophie Ebersold, Jean-Michel Bruel and Bertrand Meyer, UOOR: Seamless and Traceable Requirements, submitted for publication, February 2025, preprint available on arXiv. This article grew out of Maria Naumcheva’s PhD thesis defended on December 18 at the University of Toulouse (I will write separately about the thesis as a whole). It is part of ... Read more
Computer scienceDesign by ContractEiffelEmpirical Software EngineeringFormal methods and proofsPublication announcementSoftware engineeringSoftware verificationTestingloopsunrolling
Li Huang, Bertrand Meyer and Reto Weber, New preprint: Loop unrolling: formal definition and application to testing, February 2025, submitted to publication. Available here on arXiv and also here. Abstract Testing coverage criteria usually make a gross simplification: they assume that loops will have their bodies executed 0 or 1 time. How much (specificall,y how ... Read more
Computer scienceDesign by ContractPublication announcementRequirementsSoftware engineeringTesting
Preprint of new article: Victoria Kananchuk, Ilgiz Mustafin and Bertrand Meyer, Bugfix: a standard language, database schema and repository for research on bugs and automatic program repair, submitted for publication, February 2025. Available on arXiv here. Also available here. What this is in a nutshell (there is a longer abstract below): a proposal for, and ... Read more
Computer scienceEiffelEmpirical Software EngineeringFormal methods and proofsPublication announcementSoftware engineeringSoftware verificationTestingTheory
Just published: Li Huang, Bertrand Meyer and Manuel Oriol, Seeding Contradiction: a fast method for generating full-coverage test suites, in Springer Nature Computer Science, vol. 6, no. 4, 2025. The text is available here on the publisher’s site. Also available is a preprint version. This just published SNCS article and revised and extended from a ... Read more
EiffelFormal methods and proofsMathematicsPublication announcementSoftware engineeringSoftware verification
Bertrand Meyer and Reto Weber: Meaning as Programs — Programming Really Is Simple Mathematics, February 2025 preprint available here and also on arXiv. Theories of programming can be quite complicated; the presentation here is a return to essentials, defining programming and associated concepts (programming languages, programming methodology) entirely from elementary set-theoretical concepts. Unlike much of ... Read more
In Munich in 1938, Chamberlain and Daladier made the wrong decision, but they were driven by honorable motives. Chamberlain was weak but wanted to preserve short-term peace at all costs; Daladier was entirely lucid, but he had taken a look at the state of preparation of the French forces and wanted to buy time to ... Read more
Design by ContractEiffelFormal methods and proofsObject technologyProject managementRequirementsSoftware engineering
Bertrand Meyer, Software engineering as a domain to formalize, available here. This article is meant as a blog but was written as a standard text and I haven’t had the time to HTML-ize yet. So I am just providing an abstract below, and linking to the PDF which gives the details. The purpose is simple: ... Read more
Academic life includes self-governance and require people to sit in committees, take on various duties, serve as director of studies, graduate program director, chair of PhD chair of external relations, department vice chair or chair, dean… Not everyone wants to play. It is not rare to encounter faculty members who tell you bluntly that as ... Read more
The dominant discourse right now is “Calm down, this is just the normal game of democracy”. Actually, “this” is not the normal course of democracy. Everyone has experienced the disappointment of a favored candidate losing. The result of Tuesday is something else, not seen before in our lifetime: the triumph of indecency and the rout ... Read more
This week, Informatics Europe, the association of European computer science departments and industry research centers, is holding its annual ECSS event, bizarrely billed as “20 years of Informatics Europe”. (Informatics Europe was created at the end of 2006 and incorporated officially in 2011. The first ever mention of the name appeared in an email from ... Read more
Reading notes. From: Quelques éléments d’histoire des nombres négatifs (Elements of a history of negative numbers) by Anne Boyé, Proyecto Pénélope, 2002, revision available here; On Solving Equations, Negative Numbers, and Other Absurdities: Part II by Ralph Raimi, available here; Note sur l’histoire des nombres entiers négatifs (Note on the History of Negative Numbers) by ... Read more
Recently I prepared some of my books for free access on the Web (after gaining agreement from the publishers). Here are the corresponding links. They actually point to pages that present the respective books and have further links to the actual PDF versions. Although the texts are essentially those of the books as published, I ... Read more
Computer scienceConcurrencyDesign by ContractEiffelEmpirical Software EngineeringFormal methods and proofsObject technologyPublication announcementSoftware engineeringSoftware processSoftware verificationSoftware designTestingTheory
July 14 (still here for 15 minutes) is not a bad opportunity to announced the publication of a new book: The French School of Programming. The book is a collection of chapters, thirteen of them, by rock stars of programming and software engineering research (plus me), preceded by a Foreword by Jim Woodcock and a ... Read more
[English version forthcoming.] Que peut-on faire ? Un pays vieux d’un millénaire et demi est en train de se suicider. Pour tentant que soit le désespoir, il est encore temps d’agir. Le pire scénario, c’est la menace de la gauche. Ce qu’il restait de sociaux-démocrates s’est prosterné devant une bande d’extrémistes décidés à détruire toute ... Read more
What is going on? In the US, the leading presidential candidate is a vulgar crook, a serial business failure and convicted business fraudster; more ominously, he acts like a vassal to Putin. His first term was an endless string of catastrophes, including the deaths of hundreds of thousands of his compatriots through gross mismanagement. And ... Read more
A few years ago I was driving on a freeway in France and turned on the radio, chancing on France-Culture. (In passing it is fair to note the abundance of quality programs on that station. It has its share of empty Parisian intellectual chit-chat but much of the time I learn something interesting.) I was ... Read more
I was recently looking at the math exercises of a 14-year-old, having to do with quadratic (second-degree) equations. The first thing that caught my eye is not a surprise: the difference between school and life. The quadratic polynomials appearing in the exercises, such as x2 – x – 6, all happen to have integer roots ... Read more