Ghostty 1.0 (🔥 Score: 153+ in 45 minutes)

Link: https://readhacker.news/s/6k7S9
Comments: https://readhacker.news/c/6k7S9

A paper to spend a weekend with: https://arxiv.org/abs/2012.02113

Entropy and diversity
T. Leinster

MetaOCaml: Ten Years Later
Oleg

https://okmij.org/ftp/meta-programming/design-10.pdf
https://okmij.org/ftp/ML/MetaOCaml.html#design-10

You could have invented Fenwick trees
B. Yorgey

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/you-could-have-invented-fenwick-trees/B4628279D4E54229CED97249E96F721D

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.

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