Hacker News: danilafe

New comment by danilafe in "Principia Mathematica is modern and insightful"

danilafe — Thu, 13 Aug 2026 13:41:12 +0000

This was my first thought when I saw the article.

New comment by danilafe in "Pixel Watch 5"

danilafe — Thu, 13 Aug 2026 01:15:57 +0000

> GPS is covered by the phone that you're going to be carrying anyway

Unless you go for a run, for example.

> Really the only missing part is NFC payments.

And custom applications, not the least of which are navigation tools like Google Maps or Citymapper.

New comment by danilafe in "Pixel Watch 5"

danilafe — Thu, 13 Aug 2026 00:35:27 +0000

Well, right, that's why I said "advanced" health tracking. A pedometer is enough to measure steps.

And then, I dunno. We've clearly made this trade-off before with mobile phones. As much as I like the Nokia I had that went weeks without a charge, I also rarely notice the charging time of my phone.

Lately I've been thinking about a mode in which a "smartwatch" serves as a fitness tracker, heads-up display, and wallet, while a real, mechanical watch, which never runs out of battery, becomes the timepiece (and fashion piece?)

New comment by danilafe in "Pixel Watch 5"

danilafe — Wed, 12 Aug 2026 23:01:09 +0000

For me, the appeal of the smartwatch is more advanced health tracking, custom applications, NFC, and GPS. As far as I know, Pebble lacks most if not all of these features. I really want to want a Pebble, but it's far closer to a customizable watchface than even a Fitbit. On the other hand, daily charging of smart watches is completely outrageous.

New comment by danilafe in "U of Michigan drops first-semester grades to ‘curb mental health crisis’"

danilafe — Wed, 12 Aug 2026 13:47:57 +0000

7:30 is consistent with my experience in Oregon. Work does not count in lieu of volunteer time if you're writing an essay about your involvement with the community. I don't think schools NEED both ACT or SAT but you only have so many shots and may have an affinity for one or the other, so people like to take both.

New comment by danilafe in "OnePlus halts operations in USA and Europe"

danilafe — Thu, 16 Jul 2026 12:26:09 +0000

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

New comment by danilafe in "Claude Fable 5"

danilafe — Wed, 10 Jun 2026 04:33:49 +0000

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.

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 23:23:53 +0000

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.

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 22:43:55 +0000

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.

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 22:41:04 +0000

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/

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 20:26:27 +0000

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.

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 20:04:53 +0000

> 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.

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 20:00:10 +0000

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.

New comment by danilafe in "“Why not just use Lean?”"

danilafe — Mon, 27 Apr 2026 18:17:58 +0000

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.

New comment by danilafe in "Generating Flashcards from PDF Underlines"

danilafe — Fri, 17 Apr 2026 16:58:27 +0000

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.

New comment by danilafe in "Heathrow scraps liquid container limit"

danilafe — Tue, 27 Jan 2026 05:08:36 +0000

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".

New comment by danilafe in "Ask HN: Share your personal website"

danilafe — Thu, 15 Jan 2026 06:04:08 +0000

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.

New comment by danilafe in "Vanity activities"

danilafe — Sun, 07 Dec 2025 23:47:54 +0000

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".

New comment by danilafe in "Vanity activities"

danilafe — Sun, 07 Dec 2025 23:46:24 +0000

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

New comment by danilafe in "Vanity activities"

danilafe — Sun, 07 Dec 2025 18:58:44 +0000

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?