black_knight

For me it has the opposite effect. Now I can finally use whatever programming language I want! Is my language missing a library? No worries Opus will write one!

Buy a domain, then you don’t lose your address if you ever decide to jump to a different provider. I use fastmail currently. But I also keep my own backups.

Spain during the revolution?

No, it is a matter of degree, it is not a binary thing. It is a measure we can put on government. It is not the only thing which matters, but there are differences between governments today. One is not the same as the other, just because none of them are ideal.

“ it turns landowners into renters from the government.”

With the caveat that “the government” should somehow represent the will of society (I know, basic democracy seems like a big ask today), this seems like how it should be. The land belongs to us humans together, and if someone wants to control it exclusively, there should be something in return for the rest of us.

Yes, this is like something I would do for a DnD bit. But I have this experience often, that LLMs will suggest the easy toy version of doing something. But it knows the real stuff too, it just needs the right kind of prompting. A keyword or two, and it will find the _real_ solution.

The class system… such a classic!

Ah, yes, the cost of the price is rarely considered. Think of the money society would save just in not having to pay up for the payment system!

All models still gets things wrong. Even Fable 5.1 I have to regularly correct when working on sufficiently complex code. So, I still want models to get smarter!

Fable is good, especially at conceptual stuff, don’t get me wrong, but it has limits. Opus 5.5 is a machine at getting correct code out once the concepts are in place. But I can’t trust either to not make mistakes.

One could always copy things without credit. It was always up to people to have ethics and cite their sources.

While we should hold AI companies accountable, I feel like this one is on the person making the LLM generate, without also making it come up with sources (which it can do!)

And here is another short and simple example of some Agda code (Did you know you can open modules in a type signature‽):

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

Not sure if all the unicode characters will render on HN, but the things left of the ⟪ ⟫-brackets is exactly what a text book in mathematics will have. While the things inside the brackets are just a functional-programming way of saying out the argument which would be left for the reader to make in their head for why each step holds.

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

We are spoiled in so many ways by Haskell!

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 have hear people make this comparison many times, but it just does not hold up under scrutiny.

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.

Then you will compete on different things, i guess. For audio hardware, the physicality and experience of using it is important. Have better knobs, better usability, and the best algorithms!

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.

I feel incredibly lucky to have 25 years of computer and programming experience before the LLMs arrived. All the things I have learned through hard experience and curiosity!

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.