danilafe

Still running on OnePlus 5. The ideal phone in my opinion.

Just threw a problem at Fable that I haven't been able to get any other model to get done: porting a long-standing Agda codebase of mine to Lean, while staying faithful to the representation. In an hour, it ported ~6000 lines of Agda and everything seems to work. Lean checks out, the output is right. I'll have to study the proofs but I am very impressed.

Also true. The slowness is relatively unpredictable, too: sometimes changing a 'rewrite' to a 'with' can increase memory usage tenfold.

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.

To be fair, Coq has ProofGeneral and Agda has its emacs mode. Once you go outside these established channels, oftentimes using the tool becomes incredibly difficult. I guess for interactive theorem proving in general you may need some sort of editor at some point.

I think what holds Agda back from being "practical" is that it just doesn't have good tactics. You can't easily automate proofs and even simplification techniques require some language-level tricks[1]. There's technically support for elaborator reflection (as in Idris) but it's painful and impossible to debug. Certainly nowhere near where Coq and Lean are.

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

I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + tooling combination). Agda worked out of the box with macOS homebrew. Agda's docs are petty bad, but I've found its cross-linked module documentation incredibly useful. The main issue is knowing something exists.

The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect

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.

Its parameterized modules, extremely elegant yet flexible mixfix notation mechanism, the various niceties around pattern matching (though this one might be a bit of Stockholm syndrome; Agda doesn't nicely allow pattern matching anywhere except at function clauses), the fact that records, GADTS, and modules all feel like aspects of the same thing, and the fact that typeclasses are 'just' records that are automatically filled in. The typeclass and module features IMO already give it some edge over Haskell. I don't know if it's friendlier, but it is more ergonomic.

People tell me Lean is really good for functional programming. However, coming from Agda, it feels like a pretty clunky downgrade. They also tell me it's good for tactics, but I've found Coq's tactics more powerful and ergonomic. Maybe these are all baby-duck perceptions. So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.

I suppose it's because the tablet I'm using (reMarkable 2) doesn't have a way to intelligently track what I marked up. Perhaps it's part of their intended design.

This is funny because just a few months ago, I was forced at Heathrow to chug -- not allowed to pour out! -- my entire water bottle that I had filled prior to my flight. The security person watched me do it and added, "bathroom's over there".

I'm over at https://danilafe.com.

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

You might be right, but I was taking that as a given since the article made that claim. I think the general point (of taking smaller actions in lieu of more effective but costly ones) matters more so than the individual "vanity activity".

Yes, but only if you would spend that time on something that is more valuable (according to your happiness+ heuristic).

It doesn't have to be one or the other. Both ethical consumption and going vegetarian reduce one's environmental impact, and they're independent of one another. So, while someone "truly" optimizing for environmental impact would better spend their time avoiding meat, someone who enjoys meat can still reduce their environmental impact without becoming miserable. Variables like "income" and "environment" are just parts of the equation for the more important heuristic of happiness.

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?

I keep seeing Ghostty in the news, and I've tried it, but it feels like just another terminal emulator to men. This coming from someone who spends 90% of the workday in the terminal.

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

Their most most recent update replaces all this with a list of recently updated PRs and issues. I've been learning on it heavily since it came out. One of the few recent changes that really feels like a clear improvement.

As a sibling comment said, it's a C major chord, but voiced one noted at a time. "usually" / in pop, you hear all the notes at once.

I've had a reMarkable 2 since 2020 or so. To be honest, the only area of the device I have ever wanted to be hackable was the sync API. I am completely satisfied with the gestures, e-reader and pretty much everything else. But what I'd love to be able to do is to access my files, stored in the cloud, automatically. My use case in particular would be something that passively converts my scribbled annotations into other things.

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.

This is a strange article to me. I've not seen any class that teaches Prolog place these constraints (use recursion / don't add new predicates) or even accidentally have the outcome of "making prolog look tedious". What's the joke here?

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.

Woah, it's amazing to hear from you in person.

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.

Thank you for your thoughtful comment!

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.

My site (OP) actually has a content graph as well, though it has a dedicated page. I didn't want to force users to run arbitrary JavaScript on every page just for aesthetics.

https://danilafe.com/graph/

Taxonomies[0] are the way to go if you'd like to group content on your site by something like series (although you could "just" use tags, which Hugo enables out of the box). I use "series" as a taxonomy, for which an initial bit of code is here[1]. Given that, depending on how comfortable you are with Hugo templating, you could probably use `.Site.Taxonomies.series` to iterate over all the "series".

[0] https://gohugo.io/content-management/taxonomies/

[1] https://dev.danilafe.com/Web-Projects/blog-static/src/commit...

The idea is great, though I think I personally would prefer for this to happen on the server side (during rendering a static site, perhaps), not in the user's browsers. Particularly if the user doesn't enable JS, or has a slow connection.

Tastefully displays the most relevant citation at the bottom of the screen as you read, e.g. see https://redsails.org/really-existing-fascism/

This is very nice; I think the same can be achieved with general footnotes (not just source links), though you'd have to be careful to keep them short lest you take up a lot of screen space.

It's not signaled / warned about by default. However, if you want to make sure your `foreach` loop runs on the GPU, you can use the `@assertOnGpu` attribute. For instance, the following program would not compile:

  @assertOnGpu
  foreach i in 1..10 { /* Do something that can't be done on a GPU. */ }