Just reading chain of thought traces for Agda (I'm using Qwen 3.8-Flash-Next) and it's struggling so hard with just the syntax, long before it can struggle with semantics or type errors.

Admittedly I'm not much better, Agda has some crazy scoping rules at times and its operators are a mess, so much worse than Haskell, but at least I don't have to re-learn from scratch after every compaction.

▲

icrbow 11 hours ago | parent | next [-]

Opus 5.5 has no problem with Haskell in any domain whatsoever, including mixing it up with FFI and eDSLs. You call it, it does it.

▲

mietek 13 hours ago | parent | prev | next [-]

No, Agda's mixfix operators and general syntactic malleability is state-of-the-art in programming language design. Try learning how to write it yourself, before relying on LLM to write it for you.

▲

3836293648 12 hours ago | parent [-]

It's a cool hack. It's also a catastrophe for actual usage. State-of-the-art doesn't mean good, it just means new, shiny and complex. Not being able to do syntax highlighting without a full typechecking pass is a usability nightmare.

Anyway, that's not the part I the human struggle with, it's remembering what level of infix each new custom operator has. Why λ() isn't equivalent with λ{}, if `a b , c` is `(a b) , c` or `a (b , c)` with this version of comma (Though now I've given up on the others and just use Σ a (λ _ -> b) for all kinds of tuples just to make it consistent). Why implicits won't unify as I expect them to. Why with just doesn't work in a reasonable fashion at all ever beyond the most basic two cases (no nesting and only nest in the final case). Literally copy pasting from the docs doesn't parse.

Cool trick, but in practice it was a mistake and Haskell's take on custom operators was far enough.

▲

mietek 11 hours ago | parent [-]

Here are some resources to help you get started.

An Agda course taught in Padova since 2024: https://agdapad.quasicoherent.io/~Padova2026/

"Programming Language Foundations in Agda", a course taught at multiple universities since 2018: https://plfa.github.io

Conor Titania McBride's lectures on Agda, including videos: https://github.com/pigworker/CS410-18

Thorsten Altenkirch's lectures on computer-aided formal reasoning using Agda: https://www.cs.nott.ac.uk/~psztxa/g53cfr

▲

3836293648 4 hours ago | parent [-]

Or maybe consider being less patronising and realise that Agda is a mess, regardless of how cool some aspects of it is.

I am returning to the language, not new.

▲

mietek 3 hours ago | parent [-]

There's certainly many things that could be improved about Agda, but they mostly have to do with its semantics. Here's a great blog post about some of them: https://jesper.sikanda.be/posts/why-not-a-core-language.html

Operator fixity is a non-issue; if you don't like how the fixities have been set up, you can change them at will, even in the middle of an `import` statement. Nobody is making you use custom infix operators, either; you can write Agda that looks mostly like a Lisp if you wish.

Improving `with` is ongoing work; there was a presentation on it at the recent Agda implementors' meeting.

There's real people with real feelings building Agda, and not very many of them either. Consider that before publicly denigrating their work, with such shallow criticism to boot.

	▲	3836293648 3 hours ago \| parent [-]
		Yes, and I know some of them and have critiqued it in person.

▲

calebkaiser a day ago | parent | prev [-]

Yeah I know this pain. I actually have had some success by giving the agent a style guide for Lean that is strictly not conventional. The nice syntactic shortcuts and different modes that make Lean more ergonomic for humans, in my experience, actually make it easier for an agent to trip itself up.