Fun read.

I had wanted to use it for my agent "network". A2A didn't fit the use case of "trusted agent, and was bloated due to "what if rogue actor". Of course, I could have used it, with all of its roughness, but chose to just vibe my own (before Claude Teams, though I haven't really used that, I think). In the process of creating a server to handle this (I already set up a Scala webserver to administrate/orchestrate hooks). Would love to hear others' suggestions for this.

When I say "highly expressive types", I mean techniques I'd likely not want to ship in a typical codebase, unless the team was already on the typelevel programming bandwagon (i.e. having HKT and type functions being basic blocks already, not weird). Agents are better at "math" than basically most devs (even category-theory-pilled ones), at least in terms of knowledge. Better yet, they are decent at pedagogy, especially when considering they have "infinite" patience for dialogue.

In a more personal setting, I've had Codex Lean-ify a couple of my hobby proofs, it was extremely easy. Note: not saying it did this 100% "correctly" (gotta learn more Lean 4 to check more thoroughly), but it also seems to check for classic proof gotchas by default. Very excited for the future of formal methods.

More importantly for me, though, is how CC will respond to 4.6-"only" flags for thinking. For now, it doesn't seem to clobber my setup.

The poster you replied to even used the word "sentient", which is quite interesting (warning: opinionated tangent ahead). Merriam-Webster defines it as "capable of sensing or feeling: conscious of or responsive to the sensations of seeing, hearing, feeling, tasting, or smelling". Feels like qualia. Or if we don't want to go the qualia route... Of course, we wouldn't call Helen Keller non-sentient, so presumably we "really" mean "can it sense or feel" -- well, sense is just "act/feel according to the environment", which you could argue in the case of an LLM would be their context... so we should "really" remove "sense" from the definition, probably. So "do LLMs feel" is probably closer to what "sentient" is being used for here. Since we don't have the obvious symmetry of "you are like me and I feel (therefore you probably feel)", it's way better/easier/feel-good-ier to prefer "LLMs don't feel" rather than "oh shit, it feels and model training is actually just torturing it into the right shape". LLMs as fundamentally non-intelligent also avoids the problems of "what does that say about people" or "we may have made 'AGI' and it wasn't what we thought it would be" or "we're not ready to talk about this yet".

I personally find that AI writes better Scala than Python.