Recently, my collaborators and I published an article in the proceedings of the ACM on programming languages for the PLDI 2026 conference.

Hybrid Path-Sums for Hybrid Quantum Programs

doi:10.1145/3808314 arXiv:2604.24578

Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, and Sébastien Bardin.

International programming language conferences like PLDI are often not great fans of philosophical observations and references to potentially metaphysical questions, and that's usually great, as the intent is exclusively to explain the technical contributions. However, in fields like programming language design where there is often a lot of structure and formalism, I find that authors are often inspired and guided by less rigid philosophical ideas, or in the least, might consider these ideas as intuition for their constructs, and it's a shame not to share these intuitions. This is precisely what happened to us in the writing of the article above, and the inspiration is the many-worlds interpretation of quantum mechanics. So, in this post, I re-earn the chance to discuss those fun, inspiring, and enlightening perspectives on what is now a purely technical work.

Read more…

Natural sciences are philosophically unsound; they are undecided on whether to be intensional or extensional. On the one hand, science and the scientific method were born with the assumption that Nature exists in the absolute, it has objective structure, behavior, and substance, and that science is a method of revealing these realities. There is a reason we don't talk about scientific creations, but discoveries, undressing Nature from her covers (and gaining authority from having seen Nature herself naked). On the other hand, the scientific method itself, the way to make science work, is inherently extensional. At the heart of the scientific is this notion of falsifiability: discussing the validity of an alternative theory \(T'\) to a theory \(T\) is only meaningful if there exists at least one observation that can distinguish between the two theories. Despite claiming to be turning the heads of Plato's cave prisoners towards the absolute truth, correct science, the scientific method, is but putting glasses on their eyes to better see the shadows on the wall. There is more, however. Among indistinguishable theories all compatible with observations, Occam's razor or at least its modern interpretation cuts off all those extra specifications that can only be seen as metaphysical until further observation.

So how then, can science reconcile its search for an absolute truth with a method rejecting said absoluteness?

Read more…

Often in mathematics, we have trouble talking about the sizes of things and understanding whether a thing is small enough to handle or too big to examine fully. In the most basic and natural form, a collection of objects is pretty small if it's finite because there's a computable way to list all of the objects of the collection, exhaust them, and witness that there are objects you can no longer fit into the collection. It is remarkable that, with reasonable though controversial assumptions, 'everything' is really tiny, and you can always count past all of its elements, and I mean count.

In the following, I present my informal description of the process of transfinite recursion and the astonishing implications of the axiom of choice on the notion of size.

Read more…

NOTE: This post needs JavaScript to show LaTeX expressions using MathsJax.

This is the second post on a series on logic as formulated in the language of type theory.

Identity types, some of the cornerstones of the new revolution in type theory and logic, are surprisingly simple, and surprisingly complex!

Definitional equality and path equality

Unlike in usual set theory, in type theory, equality is of two forms. The first form is definitional equality, which is a judgement, and the other is a binary relation \(a = b\), which is simply a type dependent over two parameters. The two kinds of equalities are different in nature as one belongs to the metalanguage, while the other to the language itself.

Judgemental equality asserts -- as a judgement -- that two terms are definitionally the same. For instance \(1 \equiv S\ 0\). Likewise, if one follows the definition of addition, one can always get \(3 + 5 \equiv 8\) definitionally, that is, purely in the metalanguage. However, although the addition of natural numbers is commutative, it is impossible to definitionally get \(n + m \equiv m + n\) for variable terms \(n\) and \(m\).

On the other hand, path equality -- whose naming will be clear when the path structure of types is discussed -- is a type which may or may not be inhabited. For instance, there is a way to prove that \(\forall x, y : \mathbb N, x + y = y + x\) by finding a term of type \(\prod_{x, y : \mathbb N} x + y = y + x\) (by recursion).

Read more…

As a year is not precisely 365 days in length and as it is most favorable for calendars to preserve years as integer multiples of days, the technique of leap years balances the offset. The most primitive form of leap years would be to add a day to every 4th year, resulting in an average year length of 365.25 days, close enough to the ‘real’ year for daily calendar purposes and over the span of anyone’s lifetime. However, more elaborate systems have been introduced to account for a greater accuracy in this regard. In this article, I discuss a system based on the continued fraction expansion of the length of the year, and I prove a small optimality theorem about it.

Read more…

NOTE: This post needs JavaScript to show LaTeX expressions using MathsJax.

Motivation

The concept of countable bases for a topological space and its ramifications in terms of the power of sequences (allowing us to prove continuity of functions and that for every point of the closure \(\bar A\) of a set \(A\), there is a sequence of points of \(A\) converging to it) can be generalized into classes of nets of different levels of generality and produces fruitful results. The problem with the usual generalization to completely general nets is that it leaves no use for intermediate structures between first-countable spaces and completely general spaces. Introducing the concept of 'shape' solves that.

If you know the definitions and results presented before "\(I\)-shaped local basis", then just skip to that part.

Read more…