black_knight

We are all different, and have different challenges in life to overcome. That’s life, as they say. You, for instance, have your prejudges to struggle with.

The question is how we all deal with these challenges, and how we meet people who are different from ourselves. I think it is important that we don’t put each other down, or judge based on our assumptions of what a person’s differences entails. Meeting people as individuals, and imagine other people complexly. And cheering on each other as we each overcome our challenges.

This is exactly it. I do not at all feel superfluous in my coding endeavours these days, even when I don’t write any code. If left to its own devices, Opus 5.5 would still fail at the things I want to achieve. It would produce what I would call the toy rocket, when I want the real NASA design. And it requires constant effort in my part to keep it on track to success.

It matters because they used to be just dumb, but now they are at the same time smart and dumb.

I can work on ideas with LLMs, even within my own area of expertise. They know quite a lot, and can take an idea I have and run with it. I would never trust them to be correct, but if I give them a new idea and ask them to work out details and raise any issues they find, I can quickly evaluate their findings, and take them into account when developing the idea further.

I do not do this on all ideas, not even most. Most of the time it is still me, a sheet of paper or some code. But still, comparing to how it was a year ago, it is night and day!

A year ago I would just close the window after the first reply, shaking my head at its stupidity. I can still get that experience by using anything but Opus 5.5 or Fable. I tried the $20 ChatGPT tier last week and was immediately thrown back to that old annoyance! (I am sure the best OpenAI models are fine)

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.

In some countries, healthcare has nothing to do with “insurance”.

This is true!

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!

I have used LLMs a ton with Haskell! Opus knows Haskell really well, and it can do things very quickly in it. And in my experience the code it produces has very few bugs.

Interesting! My experience is that Claude has a tendency to always suggest the true and tried, but likes off-center ideas when I present them. Fable especially has a "yes, and!" attitude where it understands and plusses the idea.

Leans proof checker is not polynomial time, unfortunately. It is super exponential. Basically, because it can verify the result of any function it can prove to be total.

I guess the site scrolls smoothly in a TUI browser?

What are you on about? I have had Fable come up with new shit for me several times (I do research for a living, so actual new shit nobody knew before), and each time it was perfectly understandable.

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!

My Haskell experience on NixOS is wonderful!

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

It really is a great imperative langue! The IO monad is basically a better C, if you know how to wield the FFI.

> I think everyone who enters academia goes through this phase of disillusionment. This thing you revered so much as this temple of knowledge turns out to involve the same kind of human business you see anywhere else

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.

I can see why this comment would trigger people's AI alarm, especially if it fits a pattern for this user. The questions seem legit at first glance, but completely uninteresting. Too general and specific at the same time, if you see what I mean.

Something really rubs me the wrong way about automatically limiting people in science based on a number attached to their name. Seems like a very slippery slope!