jswny

Does anyone do TLA style distributed systems verification with Lean? Curious the experience there and how well supported it is

Unfortunately I’ve used Claude and GPT models for a long time in a variety of harnesses and I agree with you and I think it’s the compaction.

For some reason, codex compaction is like black magic. I’ve never felt like I can just one one continuous thread with other models, Claude I carefully curate when I compact

I agree with some of Kelley’s takes, but the issue is the tone.

Does anyone think that if Bun had been rewritten from Rust to Zig that a member of the Rust core team would have written a personal hit piece against Sumner (while pretending it isn’t a hit piece)? Probably not.

Kelley can write what he wants, but as the BDFL of a rising programming language, people are allowed to react if they don’t agree with the public image being portrayed by Zig.

What’s the advantage of that for building?

Why not WASM?

Codex is fully open source…

You want to use the model that is potentially giving your data to the government vs the one that’s openly rejecting that partnership?

Package a skill with your CLI itself and give users instructions on how to install the skill properly. That allows the agent to read the instructions in a context efficient way when it wants to use the CLI

Plenty of MCPs require you to install and run them locally, like I said remote MCP has a real advantage over CLI tho

MCP loads all tools immediately. CLI does not because it’s not auto exposed to the agent, got have more control of how the context of which tools exist, and how to deliver that context.

MCP is fine, particular remote MCP which is the lowest friction way to get access to some hosted service with auth handled for you.

However, MCP is context bloat and not very good compared to CLIs + skills mechanically. With a CLI you get the ability to filter/pipe (regular Unix bash) without having to expand the entire tool call every single time in context.

CLIs also let you use heredoc for complex inputs that are otherwise hard to escape.

CLIs can easily generate skills from the —help output, and add agent specific instructions on top. That means you can give the agent all the instructions it needs to know how to use the tools, what tools exist, lazy loaded, and without bloating the context window with all the tools upfront (yes, I know tool search in Claude partially solves this).

CLIs also don’t have to run persistent processes like MCP but can if needed

Can you explain what’s so different about pro?

I’ve used everything frontier model and had Pro a while ago but it seemed to just be the same models served faster at the time.

How do you get sub agents to work?

That’s just spawning multiple parallel explore agents instructed to look at different things, and then compiling results

That’s a pretty basic functionality in Claude code

What’s the point of having a public GitHub repo with PRs enabled if they will never merge any of them?