The POSIX shell has whacky semantics as a programming language... cs.pomona.edu/~michael/pap...

Hmm...well, it looks like I will be going out of town for a week, leaving Monday and returning Saturday June 13. If you're in the Sacremento region at the time and wanna meet up, hit me up.

Me: [shouts a stream of inventive profanity] Mom: Good news?

I often think about this article, and how since 2016 Microsoft's horrible LSP became the accidental default protocol for editors, which makes it a hurdle to do...well, anything useful with LSP, really...

Project Mage is such a wild idea, even if it never amounts to anything other than a bunch of fascinating blog posts, it's still fun to think about. project-mage.org

My God, Kevin Buzzard is such an insufferable, proudly ignorant, myopic troll... leanprover.zulipchat.com#narrow/chann...

I've been trying to maintain a "weekly log" just to track what I've been accomplishing each week. (Not nearly as much as I would like!) I don't know how long I will maintain the practice, but it's interesting looking back and seeing what I've accomplished. pqnelson.github.io/weekly/

Don't leave us in suspense: who won the fight? P? Or NP?

I couldn't help but chuckle when @velshi.com referred to him as "Fortheloveofgod Demott" 🤣

"The architecture lesson I took from this: when your substrate has the right primitives, you don’t need to build your own." Good lesson. remenos.codes/building-on-...

Brouwer: "THEOREM: Absurdity of absurdity of absurdity is equivalent to absurdity" That's it, that's the tweet.

I don't think people adequately grasp how much will be irrecoverably lost due to AI in the next decade or so... www.fastcompany.com/91549609/the...

I could not be more thankful for David Carlisle's answers in TeX.stackexchange about the inner workings of the LaTeX kernel, and all the edgecases to cryptically named helper macros 🥰

My god, why does everything have "DDos guards"? Is this because AI bots are so poorly programmed, they are DDos-ing academic journals?

Alright I have collated my notes on the Unicode standard, and it's rather convoluted character model. Now, uh, why did I need this again? Hmm...oh well, I guess it might be useful later.

I wish every Standard, Specification, and formal definition includes a BiBtex entry for itself as part of its text. Also, the ISBN used by Unicode 17.0 (978-1-936213-35-1) does not seem to actually be recognized by the organization administering ISBNs!

Last day of class at #Caltech for graduate students and seniors :'(

The Devil take this Constructive Mathematics, and all its "decidable" madness!

What even is the history behind "decidable equality"? I know Heyting's 1930 paper formalizing Intuitionistic Logic had a rather interesting digression distinguishing intensional identity, equality, and defined equality. Then [some stuff happened]. And now we have a notion of "decidable equality".

It seems I was a bit hasty in describing how "easy" it is to prove equality is decidable. First, you need to prove equality of natural numbers is decidable (easy). Then, you need "Rank(x)<>Rank(y) implies x <> y" or "x = y implies Rank(x) = Rank(y)" (again, easy). Then it's an induction argument.

This book by Wallen is a lot harder to track down, especially since neither Google nor Duckduckgo will show results concerning it. Also, a minor thing, but the articles citing it err in the year: the publication year (of Wallen's book) is 1989, not 1990.

Intuitionistic logic has "decidable equality", which is just the usual equality axioms + "for all x, y we have either x=y or not(x = y)". This *feels* anti-constructive...for algebraically closed fields, it *is* anti-constructive (you recover classical logic). For PRA, everything's fine, though.

Mom: The New York Times has assembled an Auguste committee to tell us who to vote for, for governor. [looks at names] I don't know if these people are on the committee or running for governor...

For $200bn, we could address the Hanford site leaking radioactive waste, once and for all. Or we could waste it building data centers no one will use. Whatever. en.wikipedia.org/wiki/Hanford...

I ran into a team on the #Caltech #ditchday "amazing race" spin-off contest while on the bus ride home. They were trying to make it to Echo park. I gave them some help to get to Del Mar metro station. I hope they won, but I don't know how to find out.

After reading about a quarter of the Democratic post-mortem, it's clear: - they have no clue what happened in the last election, - their plan forward is to double down on incredibly unpopular Centrist policies because it worked in 1992...so it's gotta work now, right?

I realize an underdiscussed aspect of literate programming is that you need to do a lot more pre-writing than you think. It's also easy to get into the mistaken habit of writing code, then writing prose...instead of writing prose and using code as an adjunct, to formally re-state the prose.

I have to say, startpage is the most satisfying search engine I have used since Google 2006. www.startpage.com

Has anyone written any good tutorial about using LSP for an LCF-style proof assistant (or any other proof assistant)?

I wish Isabelle/HOL had an obvious way to inspect the theorems autogenerated from a datatype declaration, like the induction scheme and so on.

Well, unit testing these tactics are certainly helpful at finding bugs. Sometimes the bugs are in the software, other times the bugs are in the proof sketches I wrote on paper 😅

Read later arxiv.org/abs/2605.10902

For my European friends, 30m gallons is about 113.5m liters. I mean, I can go on and on about how AI users share the responsibility here, but none of them seem to care. www.politico.com/news/2026/05...

I am trying to write about the difference between "abstract syntax" and "concrete syntax", and I have not developed a satisfactory explanation. I can give a clear, precise definition for both, but they are *unsatisfying*. I can give motivations for both, but again... youtu.be/nrIPxlFzDi0?...

"We prefer to write functional code, as opposed to the alternative: dysfunctional code."

I'm torn between: (1) Finish writing unit tests for tactics (2) Implementing tacticals (3) Implementing a binary search tree to start supporting definitions (4) Implementing conversions for rewriting I suspect I will end up pursuing (1), but fear I might be tempted into starting (3)...

It's cute that the HOL community uses "Gamma ?- A" for goals and "Gamma |- A" for theorems. What would be a good LaTeX version of this?

Ugh, there are 5 dozen people running for Governor of California. I'll just vote for the person with the longest name. Congratulations "Livingforgod Andcountry Demott", who narrowly beat out "Voteforme Youjerks Smith".

Just pushed in a unit testing framework, and some of Pelletier's problems as unit tests for classical tableaux solver. I ran into some interesting issues with Standard ML compilers disliking raw Unicode strings, so I had to fix that. Now, every SML compiler seems happy (except maybe SML/NJ).

Announcing: Myo, the LCF-style proof assistant based on Intuitionistic first-order logic plus Feferman's FS0 set theory. It's very coarse, literally the first public commit and nothing more. But it's quite capable. codeberg.org/pqnelson/myo

It takes more than 30 pages to define substitution in FS0 for first-order logic as an object logic, I don't want to know how long it'd take to formalize CTT in FS0 🫣

Literally the subject of Angela Maxwell and Todd Shields's book "The Long Southern Strategy": it's been happening for over 60 years, dude, you're just noticing??

I actually don't think Intuitionistic first-order logic + FS0 is strong enough to define characteristic functions of sets...

In the literature on proof assistants, what exactly is meant by the phrase "meta-analysis"? I'm familiar with the notion in physical sciences, but...it just sounds weird and idiosyncratic in proof assistant literature?

When your psychic MC asks you, "Are we about to die?" ...isn't the correct answer, "You're the psychic, you tell me"? www.bbc.com/news/article...

"Above all, be motivated by love instead of fear." ozark.hendrix.edu/~yorgey/fore...

(Syntactic) unification produces the most-general unifier, if successful. This is just a substitution which is, in some appropriate sense, "initial" or "minimal". Now, the tricky part: define in sufficient generality the notion of a "substitution".

I don't think people adequately realize how intimately coupled AI is to Silicon Valley's techno-fascism... tante.cc/2026/04/21/a...

What's a good journal to submit an article about the independence of a sentence from FS0 set theory? Asking for a friend...

Uh oh, it looks like classically in FS0 the assertion "For all x, either x = 0 or there exists y, z such that x = (y, z)" is independent of the axioms of FS0. (Intuitionistically, there's no hope for it being true.)