i've been thinking about this upending process a bit (as i'm sure we all have) and the nearest historical parallel to the backlash against AI slop is the arts & crafts movement's rejection of mechanised production, from Wikipedia “Initiated in reaction against the perceived impoverishment of the decorative arts and the conditions in which they were produced” https://en.wikipedia.org/wiki/Arts_and_Crafts_movement

i like to think of Frege and the Begriffschrift like this

Boole: logic + algebra = algebraic logic

Frege: logic + functions = predicate logic

ergo, if Boole is rightly deified then so should Frege regardless of minor infelicities (which prompted type theory anyhow) -- again, apologies if this is totally misleading

Maybe I'm too much of a CLI guy (always preferred Vim & co. to Rubymine/VS Code/etc)

this is in comparison to me getting an agent to port Ruby to jart's Cosmopolitan project -- a walk in the park relatively speaking in hindsight

i'm doing opencode <-> openrouter <-> official deepseek api (i don't get the opencode hate, i like it)

how are you doing it?

am also using Kimi K3 via kimi-code

and also GLM 5.2 via ZCode

happy with all three, they're trailing frontier but i figure if i'm running GNU/Linux then i ought to favour open weights models with my €s -- reduced my usage of claude/gpt to the ~$20 tier just to keep abreast of claude_code/codex developments

My observation. LLMs find reasoning about Agda as difficult as I find reasoning about C code. I've thrown a lot of gnarly C and Ruby code at all sorts of LLMs and they have only gotten more and more impressive as frontier models have gotten stronger. With Agda, they're like "hmm, tricky" whereas for me it's an impenetrable fortress. I've asked them why they find Agda so much more difficult to write (and why they have to iterate and reiterate many many many times until they get to a destination whereas they can one-shot and two-shot C and Ruby and they tell me its the multiple competing constraints. GLM is hilarious, it flat out refuses to write Agda code but it reads it well enough. They all read it well enough. Fable is obviously great at it. And Opus 4.8/5.0 are great (if they stay on track and don't sneakily go their own way) but they're too annoying to talk to. On balance Kimi K3 is the best balance of not annoying, relatively cheap, and strong -- great model all round tbh.

So yeah, interesting I've discovered the limits of their ability coding-ability-wise. None of them are that good at designing/aesthetic judgment/architecting so thankfully they still need me in the loop.

https://youtu.be/FavUpD_IjVY

that's a weird way of describing a near frontier open weights un-crippled useful coding buddy

do you work for OpenAI or Anthropic per chance?

Source: my bank balance

these two claims can't be true at one and the same time:

(a) they're distilling our secret sauce!

(b) they'll never catch us!

I know about the guidelines, I've been on here since 2010, like yourself.

and it responded with

"Ok, I'll drop it." and stopped dead.

What makes Fable so much better than Opus besides being a better coder is that it's personality and judgment are far superior.

https://gitlab.com/igravious/lettuce.git