If you follow the field of software engineering (both industrial and academic) and like spicy writing, then do yourself a favour and read https://arxiv.org/abs/2510.24483 .

It's a wonderful, if depressing, read.

While I'm on my Epigram kick.

What I really dislike about proofs by pattern matching in systems like Agda is that after you've managed to write down the thing you need, the process by which you got there is totally obliterated. In order to figure out how you managed to match on the right things at the right times, the only thing you can do is delete the code and try again.

This is really inferior, in the sense of recording mathematical ideas, to something like tactics in Rocq or Lean or HOL Light, etc. where you can just step through the proof and see where each induction happened, and what got generalised when, etc. With the imperative-style tactic proof, you retain the sequence of proof steps, but you lose the ability to *read* those proof steps without stepping through them in the machine. So one step forward, one step back.

What Epigram's approach to pattern matching offered, which seems to have been rejected as "not Haskell/OCaml-like enough!!" by other dependently typed languages, is to *both* record the mathematical process by which a proof was refined, *and* make this process readable if printed out on a piece of paper.

Isabelle's Isar language can be argued to achieve the same goal, but in a totally different way.

Either way, this is so valuable. I think this kind of explicitness is not only important for proof engineering, but I think it is also extremely important for teaching. It is how we are going to break out of the "Mash The Agda/Rocq/Lean Keys" computer game that our students play instead of learning the mathematics.

The 'ask' system that @pigworker and colleagues are building is a great example of the direction we need to go.

If you use, expect to use, or have an opinion about using AI, you definitely need to read this. Jaw-dropping stuff.

https://amandaguinzburg.substack.com/p/diabolus-ex-machina

The pre-print for the #ICPC paper “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” by @sarantja @azaidman and yt is now available at https://sarajuhosova.com/assets/files/2025-icpc.pdf

I very much hope this will inspire more research on the usability and accessibility of the languages we build going forward!

Abstract:

Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes.

#Agda #TheoremProving #DependentTypes #Usability #Accessibility #ICPC25

"How disruptive would it be if GitHub started deleting repositories, or Google Scholar started hiding certain papers in response to U.S. government demands?"

https://www.thetransmitter.org/policy/science-must-step-away-from-nationally-managed-infrastructure/

Most people with some interest have seen precisely this coming for more than a decade. @neuralreckoning is among them. It's great that outlets like @thetransmitter are now also recognizing this problem and are helping to amplify these voices.

#openscience #infrastructure

I was literally joking about the Netherlands offering to make New York into New Amsterdam again last week.

My wish has come true!

Well done @EUCommission 👏

#USpol #NLpol #EUpol #funny #YesPlease

On Wednesday 15 January 2025 I’ll be defending my dissertation titled “Declarative Name Binding for Type System Specifications”. The defense starts at 17:00 CET and can be followed online (livestream: https://nmclive.tudelft.nl/mediasite/play/e5b66c56929044a792325e3eec3f04a31d).

A Dutch PhD defence is a very formal public ceremony. After a short presentation to introduce the dissertation topic to the audience, there is an hour of questioning by the committee members, until the bedel announces hora est (it is time). If the degree is awarded, the diploma ceremony immediately follows the defence.

The topic of the dissertation is the design of a meta-language, Statix, to support high-level type specifications of programming languages with expressive name binding features, and automatically generate type checkers from those specifications. The dissertation is accompanied by a number of propositions that reflect on the research more generally or comment on societal issues. Follow this link to download the dissertation and propositions: https://doi.org/10.4233/uuid:4bf44aa1-779c-4a96-8c55-5e1b54e16119.

Wikipedia is a problem for Musk/Trump. Not, as Musk says, because it's "woke." Because it's one of our last reliable tethers to a consensus reality. Therefore, an antidote to disinformation.

It's not making anyone money. It's not enshittified. Of course it's not perfect—it's an endeavor of imperfect cooperating humans. But it needs protection and support.

https://www.newsweek.com/elon-musk-takes-aim-wikipedia-fund-raising-editing-political-woke-2005742

#wikipedia