Viewing profile — danilafe

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 repr…

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…

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 in…

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 lang…

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…

> 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 jus…

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 syndr…

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…

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 securi…

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) sneak…

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 on…

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

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 termina…

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 th…

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

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 outcom…

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 ins…

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 t…

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…

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 …

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