danilafe · HackerTrans

в прошлом месяцеdiscuss

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.

danilafe

2 месяца назадdiscuss

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.

danilafe

2 месяца назадdiscuss

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.

danilafe

2 месяца назадdiscuss

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 technically support for elaborator reflection (as in Idris) but it's painful and impossible to debug. Certainly nowhere near where Coq and Lean are.

[1]: like this one I've used for several proofs so far: https://danilafe.com/blog/agda_expr_pattern/

danilafe

2 месяца назадdiscuss

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.

danilafe

2 месяца назадdiscuss

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

danilafe

2 месяца назадdiscuss

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 anywhere except at function clauses), the fact that records, GADTS, and modules all feel like aspects of the same thing, and the fact that typeclasses are 'just' records that are automatically filled in. The typeclass and module features IMO already give it some edge over Haskell. I don't know if it's friendlier, but it is more ergonomic.

danilafe

2 месяца назадdiscuss

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 ergonomic. Maybe these are all baby-duck perceptions. So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.

danilafe

3 месяца назадdiscuss

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.

danilafe

6 месяцев назадdiscuss

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 over there".

danilafe

6 месяцев назадdiscuss

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.

danilafe

7 месяцев назадdiscuss

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

danilafe

7 месяцев назадdiscuss

Yes, but only if you would spend that time on something that is more valuable (according to your happiness+ heuristic).

danilafe

7 месяцев назадdiscuss

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 impact would better spend their time avoiding meat, someone who enjoys meat can still reduce their environmental impact without becoming miserable. Variables like "income" and "environment" are just parts of the equation for the more important heuristic of happiness.

A lot of the activities on that list are like this. Reading the news has a non-zero impact (hey, I'm on HN, and it definitely helps me keep up to date), and it's "easy" in that it fits into my heuristic for happiness. Same with using a metal straw, and same with picking between credit cards.

In a sense, these activities are "free" in terms of their perceived difficulty, but have a positive, if small, impact. If they're "free", why not do them?

danilafe

7 месяцев назадdiscuss

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's special about Ghostty compared to alternatives?

danilafe

7 месяцев назадdiscuss

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.

danilafe

7 месяцев назадdiscuss

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.

danilafe

7 месяцев назадdiscuss

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'd love to be able to do is to access my files, stored in the cloud, automatically. My use case in particular would be something that passively converts my scribbled annotations into other things.

The API hacking scene is very much dead. Most API implementations have been unmaintained for years now and no longer work. It's a real shame.

comments