Remix.run Logo
▲ mietek 11 hours ago

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.