Alex Nelson

Is that...Gollum? "Come see my PRECIOUS...bathroom fixtures."

TOON TUESDAY
#ToonTuesday

Infinite-Dimensional Lie Groups This is a preliminary version of a book on infinite-dimensional Lie groups. It covers the basics of calculus and manifolds in the context of locally convex spaces, based on Bastiani's notion of a smoo...

Read later (a ~1026 page manuscript)...

arxiv.org/abs/2602.12362

Hilbert's Program and Infinity The primary aim of Hilbert's proof theory was to establish the consistency of classical mathematics using finitary means only. Hilbert's strategy for doing this was to eliminate the infinite (in the f...

Read later

arxiv.org/abs/2602.12131

I'm hardly the first person to note this, but it's enormously instructive that our President and his followers saw the message "THE ONLY THING MORE POWERFUL THAN HATE IS LOVE" and understood it, correctly, as an attack on them

Some people are asking what I want Schumer to do. He should be screaming over medical care and access to facilities. He should be going to detention facilities himself and putting his body on the line, as he did at the border in 2019. He should lean into stories about New Yorkers in detention. [1/4]

I just wish there were an "Algebraic Geometry for Differential Geometers" book out there :(

Edward Gibbon was far better with this type of juxtaposition, specifically to maximize irony. But I guess we can't all be a Gibbon...

I wish people would use commas.

For example: "While tropical countries will bear the brunt[,] cooler regions will also need to adapt."

You need that comma inserted for the sentence to make grammatical sense.

USE COMMAS, GOSH DARNIT.

But I don't think I will adequately get a chance to do this for about a month, because my sister and her husband are visiting until the end of February.

I was thinking about writing a post about the desired qualities ("desiderata") and design choices necessary when implementing a literate programming tool...especially since implementing a proof assistant *as* a literate program requires special concerns.

Perhaps I should write a meta-"literate program" to document the successes and failures of these explorations?

But to have found me on Bluesky, which is no small task, so I guess someone must be interested in what I have to say about it.

Ah, well, currently I am working my way through bootstrapping a literate programming toolkit. I feel the Markdown prototype was...inadequate for my needs.

Now that I am thinking about it, I suppose I am experimenting with several prototypes...

If you are serious about literate programming, I would still recommend building a Pandoc filter: you will save yourself a boat load of trouble.

Trouble is my business, so I'm still bootstrapping a literate toolkit in Standard ML to study implementing proof assistants.

What piqued your interest?

I'm still working on it (I realized too late that Markdown was inadequate for my purposes because I wanted to state theorems, and that forced *me* to *manually* write the theorem numbers and italicize the theorem statement).

I have a version of the Markdown locally, somewhere...

Every "Let's build an LSP server" starts off simple, then ends up with extraordinarily convoluted data structures by step 3 🫣

You know...from that land...from the land of the ice and snow from the midnight sun where the hot springs flow...

Concurrent POSIX file system operations has been verified in TaDa

www.doc.ic.ac.uk/~pg/publicat...

Executable formal semantics for the POSIX shell The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert's control panel, a necessary tool for configuring, compiling, installing, maintaining, and de...

The POSIX shell semantics has been formalized in Lem (which extracts to Coq/Rocq and Isabelle/HOL and other proof assistants).

arxiv.org/abs/1907.05308

UNIX Path resolution has been formalized in Why3

inria.hal.science/hal-01406848...

How much of POSIX has been formalized in a proof assistant? I know of a bunch of scattered results, but they seem to be independent disjoint efforts...

And since POSIX is a multi-volume specification, I wouldn't be surprised I don't cover everything here in one thread.

After writing a POSIX-compliant shell script, then rewriting as a literate program using Noweb, I realize I might need to use an honest programming language like Standard ML to actually implement the desired program 😅

Since it's under the 35^4 ~ 1.5e6 threshold, that's the critical thing. I'd only need to pause and re-evaluate things if there were, say, 1.5e5 such identifiers.

Things reduce a little (you get 10,385 at the top-level directory, and 44,969 in subdirectories).

I'm just trying to get a feel for things (specifically if something like Stacks tags could be used for literate programming proof assistants), so over-estimating is better than under-estimating.

To be precise, with my version of HOL Light (slightly out of date), there are 24,049 identifiers in files in the parent directory, and then 158,092 identifiers in files in the subdirectories.

(To get a sense of things, Isabelle seems to use about 32k SML identifiers in its kernel.)

I just need a rough estimate, so I decided to do something like "ls *.ml | grep -n "let " | wc -l" (and another for the subdirectory files "ls ./*/*.ml | ..."). For HOL Light, it was something on the order of 100k identifiers.

TIL ZSH is not a POSIX-compliant shell, after spending a couple hours trying to figure out why it doesn't accept my script the same way DASH, BASH, KSH, and other POSIX-compliant shells do...

Is there a way to estimate the number of top-level identifiers in an OCaml program?

Yeah, I'm not gonna lie, I am not a fan of the terminology used by Algebraic Geometers: their "immersions" aren't really what differential Geometers call "immersions" (instead AG's "unramified morphisms" are "immersions") 🫣

Greibach Normal Form Greibach Normal Form in the Archive of Formal Proofs

I just found Alexander Haberl, Tobias Nipkow, and Akihisa Yamada have formalized Greibech normal form in Isabelle/HOL a couple months ago.

www.isa-afp.org/entries/Grei...