danilafe

Beautiful! Thank you for sharing.

Not to be overly pedantic, but isn't that not "most", out of even Americans?

Surely they're referring to the llm-isms in the text?

This was my first thought when I saw the article.

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

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?)

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.

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.

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