← Feed

Posts

• Post #3804963

  When even the abstract is complete nonsense. Sigh.

• Post #2636110

  Listening to a bunch of Bee Gee's stuff right now. My, they were so good! Yes, I like them. And Lorna Shore and Rammstein and Rush and Metric and Abba and Avril Lavigne and The Hu and Nusrat Fateh Ali Khan. And so many more.

• Post #2636109

  I think I like doing work with a proof assistant for exactly the reason that drove others nuts: there is nowhere for tacit knowledge to hide. I was reminded of this while trying to read some "paper math" on type theoretical forcing. I can't just click on some bits to ask "what exactly do you mean by this part here". [The thing I wanted to know was indeed never defined, just assumed to be known.]

• Post #2636108

  It would be hilarious if what un-scaled university classes (i.e. pushed them to be smaller) was LLMs. If a class is supposed to be teaching students some skills, then we can no longer check if that has been successful "remotely" (i.e. via written assignments). So we have to check them in-person. Which takes a lot more time.

• Post #2636107

  Hard puzzle: what do Perth, Scotland and Erfoud, Morocco have in common? [Answer might be delayed, wifi connection where I am is not necessarily good.]

• Post #2239288

  Now this is the kind of software engineering research that I'd like to see more of! https://arxiv.org/abs/2602.10540

• Post #2172772

  @egbertrijke I quite like formalizations that are made to look like encyclopedia pages. I just dislike when they are made to serve double-duty, i.e. serve a narrative purpose as well as a "source code for a library" purpose at the same time. Then you're forced into all sorts of compromises. Libraries need vastly different organization than good narrative does. I don't actually care which one ends up being the primary artifact. [But my current best guess is that it's eas...

• Post #2172771

  "We present a sorry-free formalization" -- as if a document with 'sorry's in them could be called a formalization?

• Post #2172770

  When I agreed to be on the PC for conference X, I did not think I had agreed to review alchemy papers. And yet, here we are. Yes, this is about "modern AI".

• Post #2172768

  "Never hallucinate or make anything up." Sounds like instructions for the orange one at trial. Or instructions a reporter might wish to give before an interview.

• Post #2172767

  github crumbling because of AI is both sad and funny. And annoying: can't do my code reviews right now.

• Post #2172766

  Damn. I jotted down a quick idea in my research notes file (in markdown, in github, using the web edit function). Copilot auto-filled a commit message as a starting point. It was good. That is super annoying.

• Post #2035238

  I'd love it if there was a tradition of putting in an "author's version" of a paper onto the arxiv. No, I don't mean the extended version, I mean the version with all the puns, side stories, footnotes and the like kept in. And sure, the proofs too.

• Post #1666321

  This is the point of formalization: In several places, the process of formalization sharpened our understanding of the informal presentation. p. 4 of a just-landed formalization of the reals in cubical agda. https://users.cs.utah.edu/~blg/resources/pdf/jackson-brough-cubicalreals-2026.pdf

• Post #1402968

  No one who has done enough proving should ever say that a "program has been proven correct." Does it satisfy the theorems you've proven? Sure. Are they all the theorems needed to say 'correct'? Extremely unlikely!