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…
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…
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…
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…
Still running on OnePlus 5. The ideal phone in my opinion.
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…
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…
> 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…
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…
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…
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,…
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…
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…
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…
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…
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".…
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…
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…
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…
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:…
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…
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…
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…
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…
Still running on OnePlus 5. The ideal phone in my opinion.
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…
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…
> 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…
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…
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…
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,…
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…
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…
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…
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…
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".…
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…
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…
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…
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:…