https://vezwork.github.io/drostes-lair-post/

A cute cool project. If you don't understand recursion, this can help immensely. Also if you don't know what the amb is, you can and should learn.

If you already know all that, it's just a fun game. 😊

Eratosthenes again.

Turner, Bird, Eratosthenes: An eternal burning thread
by J. Gibbons

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/turner-bird-eratosthenes-an-eternal-burning-thread/32E2EDF5D5EAEC95F13D313BC97B86F0

Learn Programming with OCaml
by Sylvain Conchon and Jean-Christophe Filliâtre, 2025

https://usr.lmf.cnrs.fr/lpo/

https://calculatingempires.net/

A fascinating visualization (a timeline) of the development of communication, data management, computing, education, medicine, economy, energy, policy, surveillance, military and so on from 1500 till today across the world.

I'm not sure it's 100% historically accurate, but still illuminating.

https://www.youtube.com/watch?v=CVLSA8YGvM8

https://catcolab.org (https://github.com/ToposInstitute/CatColab)

This is mind-blowing! 🤯

A collaborative (as in Google Docs) notebook for defining and simulating a range of "logic"/diagram notations starting with purely descriptive ontologies and up to quantitative stock-and-flow diagrams (which define a system of differential equations).

Implemented in Rust and TypeScript offloading the heavy-lifting of actual processing to AlgebraicJulia and Julia's differential equations ecosystem. All based on Double Category Theory.

https://arxiv.org/abs/2502.03544
Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V. Le, Thang Luong
5 Feb 2025

We present AlphaGeometry2, a significantly improved version of AlphaGeometry introduced in Trinh et al. (2024), which has now surpassed an average gold medalist in solving Olympiad geometry problems. To achieve this, we first extend the original AlphaGeometry language to tackle harder problems involving movements of objects, and problems containing linear equations of angles, ratios, and distances. This, together with other additions, has markedly improved the coverage rate of the AlphaGeometry language on International Math Olympiads (IMO) 2000-2024 geometry problems from 66% to 88%. The search process of AlphaGeometry2 has also been greatly improved through the use of Gemini architecture for better language modeling, and a novel knowledge-sharing mechanism that combines multiple search trees. Together with further enhancements to the symbolic engine and synthetic data generation, we have significantly boosted the overall solving rate of AlphaGeometry2 to 84% for all geometry problems over the last 25 years, compared to 54% previously. AlphaGeometry2 was also part of the system that achieved silver-medal standard at IMO 2024. Last but not least, we report progress towards using AlphaGeometry2 as a part of a fully automated system that reliably solves geometry problems directly from natural language input.

https://dl.acm.org/doi/10.1145/3704912
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter

Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.

TL;DR: do not use LLMs for forecasting.

https://arxiv.org/abs/2406.16964

Termination Combinators Forever
Maximilian Bolingbroke, Simon Peyton Jones, Dimitrios Vytiniotis

We describe a library-based approach to constructing termination tests suitable for controlling termination of symbolic methods such as partial evaluation, supercompilation and theorem proving. With our combinators, all termination tests are correct by construction. We show how the library can be designed to embody various optimisations of the termination tests, which the user of the library takes advantage of entirely transparently.

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/termination-combinators.pdf

https://www.pm.inf.ethz.ch/research/verifythis.html

Another VerifyThis Competition is coming May 3rd and 4th, 2025.

Online participants are welcome: https://docs.google.com/forms/d/e/1FAIpQLScOhK5tMG5q5DMb36yrTQ8itUwvJ2EN8IG_kgjsX6HQZ6dDhw/viewform

The use of AI-based tools is allowed.

Programming Really Is Simple Mathematics
B. Meyer, R. Weber

https://arxiv.org/abs/2502.17149

https://corticallabs.com/cl1.html

A brain in a vat, but unironically... 🥴

Zero copy data structures

https://www.hytradboi.com/2025/df37d71b-0552-47f9-af36-f53c9ee09f8f-zero-copy-data-structures

Keep an eye on the conference, https://www.hytradboi.com/2025

Dear readers, you probably want to be subscribed to these link aggregator channels. Reading them for a few years, heartily recommend.

- https://www.tgoop.com/axisofordinary
- https://www.tgoop.com/j_links

The Functional Machine Calculus

Willem Heijltjes

This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with "reader/writer" effects: higher-order mutable store, input/output, and probabilistic and non-deterministic computation.

The FMC derives from the lambda-calculus by taking the standard operational perspective of a call-by-name stack machine as primary, and introducing two natural generalizations. One, "locations", introduces multiple stacks, which each may represent an effect and so enable effect operators to be encoded into the abstraction and application constructs of the calculus. The second, "sequencing", is known from kappa-calculus and concatenative programming languages, and introduces the imperative notions of "skip" and "sequence". This enables the encoding of reduction strategies, including call-by-value lambda-calculus and monadic constructs.

https://arxiv.org/abs/2212.08177

Collapsing Towers of Interpreters

Nada Amin, Tiark Rompf

Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass. In the real world, a use case might be Python code executed by an x86 runtime, on a CPU emulated in a JavaScript VM, running on an ARM CPU. Collapsing such a tower can not only exponentially improve runtime performance, but also enable the use of base-language tools for interpreted programs, e.g., for analysis and verification. In this paper, we lay the foundations in an idealized but realistic setting.

https://dl.acm.org/doi/10.1145/3158140

Specializing Data Access in a Distributed File System (Generative Pearl)
P. Das, A. Xhebraj, T. Rompf

https://dl.acm.org/doi/10.1145/3689484.3690736

https://www.youtube.com/watch?v=YeWCPRXWIuA

Modern distributed file systems partition and replicate data amongst a cluster of participating nodes to enable processing of larger-than-memory datasets and to provide fault tolerance. Typically, these systems maintain designated coordinator nodes that track the state of the cluster and route user operations to the nodes holding the requested data.

One way to improve performance in this scenario is to provide the client with the cluster topology and data distribution information so that they can bypass the designated coordinator and directly access the data. Click Me Load More the files from the underlying file system instead of having to go through high level APIs can lead to significantly better performance <...>

In this paper, we propose a system, DDLoader, that embeds the information about the data distribution into the language using the Lightweight Modular Staging metaprogramming framework for Scala. Multi-stage programming techniques allow developers to build applications while delegating the task of generating low-level file loading details to the generated code. This hides the implementation details of the underlying distributed file system while retaining the performance of handwritten examples. Further, metaprogramming erases the distinction between the data loading and data processing phases of the applications typically built over distributed file systems, allowing whole program optimization, which was not possible previously.

FP²: Fully in-Place Functional Programming

Anton Lorenzen, Daan Leijen, Wouter Swierstra

As functional programmers we always face a dilemma: should we write purely functional code, or sacrifice purity for efficiency and resort to in-place updates? This paper identifies precisely when we can have the best of both worlds: a wide class of purely functional programs can be executed safely using in-place updates without requiring allocation, provided their arguments are not shared elsewhere.

We describe a linear _fully in-place_ (FIP) calculus where we prove that we can always execute such functions in a way that requires no (de)allocation and uses constant stack space. Of course, such a calculus is only relevant if we can express interesting algorithms; we provide numerous examples of in-place functions on datastructures such as splay trees or finger trees, together with in-place versions of merge sort and quick sort.

We also show how we can generically derive a map function over _any_ polynomial data type that is fully in-place. Finally, we have implemented the rules of the FIP calculus in the Koka language. Using the Perceus reference counting garbage collection, this implementation dynamically executes FIP functions in-place whenever possible.

https://dl.acm.org/doi/abs/10.1145/3607840