While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that.

[1]: like this one I've used for several proofs so far: https://danilafe.com/blog/agda_expr_pattern/

This is a nice thought, but with Agda in particular it's just not true. It's one of the few languages I've seen that's sufficiently unrepresented in training data. Frontier LLMs (Codex, Claude Code) reliably say "I realized I can't do this." after wasting lots of tokens going back and forth.

In fact, I think this positions Agda uniquely poorly.

It's a blog, where I write about compilers, formal verification, and programming languages mostly. Occasionally some web design (with Hugo) sneaks in.

A lot of the activities on that list are like this. Reading the news has a non-zero impact (hey, I'm on HN, and it definitely helps me keep up to date), and it's "easy" in that it fits into my heuristic for happiness. Same with using a metal straw, and same with picking between credit cards.

In a sense, these activities are "free" in terms of their perceived difficulty, but have a positive, if small, impact. If they're "free", why not do them?

Asking in good faith -- could someone tell me what's special about Ghostty compared to alternatives?

The API hacking scene is very much dead. Most API implementations have been unmaintained for years now and no longer work. It's a real shame.

That aside, I wonder if getting the reverse solution (sum(?, 10)) is better served by the straightforward or the tedious approach. I suspect both would work just the same, but I'd be curious if anyone knows otherwise.

> Gwern.net has it! It's just that because we use both margins already, there is usually not enough horizontal space.

Upon closer inspection, I do. I should say that I have missed it up until now, though. Some sort of selective blindness, probably.

> Chrome has a 'link to text fragment' feature for this which got standardized and which Firefox is supposed to support at some point. So not so necessary as it used to be. (The unique IDs are often not so unique anyway or unstable.)

Thank you for reminding me of this; I stumbled across it some time ago and was quite surprised. I myself use Firefox, so until it adds support for this feature, I don't think I'll be leaning on it myself (and thus will try to provide anchors).

I would say that another microfeature I love is having stable and unique element IDs :-)

> Links.js hasn't been used in years on Gwern.net.

Thank you, I was failed by GitHub search. I will update the post. I struggled to find the Lorem link when looking for it; I would've expected to at least find something on /about, but did not. I understand that it's a test page, but it does currently have the only description of what the icons mean, and as a reader I definitely could've used a description.

> But again, the page doesn't make use of the feature it is extolling the virtues of!

I said I loved the feature, not that I had the energy to implement it -- though I definitely should. :-)

> Yes, though I might argue that such links, or a link to a ToC page for the group, belong in a more general list of related links.

This is a good idea, and in my ideal world my site (and others) would support this, but it's more difficult to do automatically. Stitching together a series TOC and connecting sequences of articles is easier to automate.

> I'd stay away from an icon per target site/type though - that could quickly get confusing as you essentially have many icons for the same thing (an external link), and every site will use its own preferred set of icons, so the difference won't help generally identify things at a glance.

Yes, I'm not sure that I'd advocate for this in general. Another issue is that I personally get a little confused by some of the icons (what does "SAMA" stand for, if you don't know about OpenAI / Sam Altman already?).

> I'd like all articles to carry an obvious date of publishing and/or last update

Definitely, though as others in the comments have suggested, it may be that Google downranks pages like this. Not that I care much for my search ranking.