danilafe

7 ms·

1.
by danilafe 16d ago
Surely they're referring to the llm-isms in the text?
2.
by danilafe 1mo ago
This was my first thought when I saw the article.
3.
by danilafe 1mo ago
> 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
4.
by danilafe 1mo ago
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 we
5.
by danilafe 1mo ago
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 custom
6.
by danilafe 1mo ago
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 m
7.
by danilafe 2mo ago
Still running on OnePlus 5. The ideal phone in my opinion.
8.
by danilafe 3mo ago
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 a
9.
by danilafe 5mo ago
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&#
10.
by danilafe 5mo ago
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
11.
by danilafe 5mo ago
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 techn
12.
by danilafe 5mo ago
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
13.
by danilafe 5mo ago
> 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
14.
by danilafe 5mo ago
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 anywher
15.
by danilafe 5mo ago
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 ergono
16.
by danilafe 5mo ago
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.
17.
by danilafe 8mo ago
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
18.
by danilafe 8mo ago
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.
19.
by danilafe 9mo ago
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 activit
20.
by danilafe 9mo ago
Yes, but only if you would spend that time on something that is more valuable (according to your happiness+ heuristic).
21.
by danilafe 9mo ago
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
22.
by danilafe 10mo ago
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&#
23.
by danilafe 10mo ago
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.
24.
by danilafe 10mo ago
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.
25.
by danilafe 10mo ago
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&#
26.
by danilafe 1y ago
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".
27.
by danilafe 2y ago
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
28.
by danilafe 2y ago
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. :-) &g
29.
by danilafe 2y ago
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/
30.
by danilafe 2y ago
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 a

More ›