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