-- An element has at most one two-sided inverse.
    inverse-unique : ∀ (M : Monoid) (open Reasoning M)
                       (x y z : type M)
                   → y ⋆ x ＝ unit M
                   → x ⋆ z ＝ unit M
                   → y ＝ z
    inverse-unique M x y z leftInverse rightInverse =
      begin
        y                ⟪ sym (unitᵣAt y)           ⟫
        y ⋆ unit M       ⟪ mapᵣ (sym rightInverse)   ⟫
        y ⋆ (x ⋆ z)      ⟪ sym (associativeAt y x z) ⟫
        (y ⋆ x) ⋆ z      ⟪ mapₗ leftInverse          ⟫
        unit M ⋆ z       ⟪ unitₗAt z                 ⟫
        z
      ∎
      where open Reasoning M

(If you know Agda, I dare you to look carefully at this example!)

Parser combinators alone makes monads (or really applicative functors) worth it. But then there are the all the other spectacular things we can do with monads!

I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.

But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).

These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.

Also, I guess with agents it should be possible to explore new algorithms more efficiently. You may discover something cool! And yes, anyone can copy it, but you will still have first mover advantage. Also, in music tech brands matter a lot. People love getting stuff from small “artisan” companies.

But at the same time, I am happy with my current use of LLMs. I get to do things I only dreamed about before. I would have so many ideas I could never realise. Now I can fire up Claude Code and get cracking. And because of my experience, I can keep up with it, correcting it, suggesting better ways of doing things…

And yes, so glad I have my PhD already. But I am looking forward to all the articles I will be writing based on my collaborations with both humans and LLMs.

My new favourite thing is to use records to type interfaces for more C style libraries with lots of IO. The trick is to use Generic and a type class to gather the interface into a list or similar and running that in IO using the library. Say, using a record to type audio and midi inputs and outputs in an audio plugin.

Opus can do this correctly first try, you just need to give it the idea!

Of course I don’t know how it got its ideas for what to try. But heck, I don’t even understand how I get my ideas half the time. But the process, like what code it wrote, simulations it ran etc can be understood by (some) humans just fine!

I think it depends on your district. On some distros (looking at you arch!) I think GHCup and keeping things in /home and out of your system package manager is the better approach.

That said, I never had issues with Pandoc on any distribution. But I have struggled with Pandoc extensions, before I got NixOS (and flakes).

My experience and disillusionment is different from yours. I was inspired to do research from nerdy blog posts from researchers in my field. And my experience has mostly been that people in my field are honest, hard working, genuinely interested in doing their research as well as possible – mostly to satisfy their curiosity and sharing their findings with others. Any disillusion I have experienced has been about the fact that doing research is more or less something they squeeze in between teaching, applying for money and administrative tasks.

Even critical remarks are in the spirit of "You should do this better!", never the kind of gate-keeping bullshit I have seen in other fields.