nrds

That is an analogy between one thing and another thing, but the topic of this thread is the designation of Anthropic as a supply chain risk, which is not involved in your analogy. It is traditional that comments refer to the topic of discussion in some way.

For example, one might extend your analogy to "The nuclear power plant then declares that it will not buy the pens after all, and the pen manufacturer (who had banned them as a customer) sues them to force them to buy the pens after all."

Literally every sentence dang has ever written on this site, that I've seen, is snarky.

> Yes, in the sense that if there's nothing interesting to say about a quote then there's no reason to copy it into the thread.

This one was both snarky and indignant. Indignant that anyone would post something dang doesn't like on his site, and snarky that the the original commenter hadn't conformed to norms of what positions are acceptable to utter here.

> snark and indignation

These are preference-based but you're pretending they're objective. I find _your_ comments to be full of snark and indignation more than any you respond to, but of course you won't agree. (But because you don't agree, that makes me objectively wrong, I know.)

"Tonal arguments are ways of, frankly, policing working class ways of communication, and covering them in elite preferences." - someone smarter than the average HN commenter.

The problem with this belief is that it implies that all of bigtech is massively overpaying for top talent who would happily stay on for pennies. While bigtech overpaying talent is more plausible than any other bigcorp doing so, it's still rather unlikely.

It is no coincidence that countries which need it least can unban it. Deindustrialization activists will focus their efforts on countries where the ban matters.

Exactly; this is not the product of serious legal work.

Wait until you realize that MCPs are just the APIs that we've failed to write before, and skills are just the documentation and simple CLIs we've failed to write before

Indeed, given 60 Minutes' historically fraught relationship to the whole concept of "truth", it's hard to credit the whole story.

Failure to read the room might explain why the tourists persist in the questioning beyond politeness, but not why they embarked on the quest to interrogate the worker to begin with.

My family does this and I can barely go anywhere with them for the embarrassment. Everything is an interrogation. They actually take delight in the waiter not knowing the answer to where the seafood was caught, and then lecturing them about the importance of knowing such things (this is the most common one they pull). That's not just failing to read the room.

We've been daily-driving this model for a few weeks and let me tell you, everything it does is a lot. Fast as fuck and it's actually not bad intelligence-wise for a fast model. It basically tries to make up for any intelligence deficit by just doing a lot, checking a lot, retrying a lot.

That's not to say I don't spend my days raging at it... a lot... but it's not that bad. It does tend to ignore completion criteria but it doesn't obviously degrade when being nudged like some models do.

Wait until you realize that the difference between path and query string is entirely arbitrary and decided by the server. Query strings should never have existed. They are an implementation detail of CGI webservers that leaked all over everything and now smells really bad.

You're drawing an equivalence between the wrong pair of things. I'm not saying that term=program; I'm saying that the type checker, qua `term -> context -> decision`, bound to a particular term, is a program `context -> decision`, and the other approach is also a program `context -> decision`. I guess it's defunctionalization, not "nothing", but a next-door neighbor of "nothing".

So you're telling me that cells use an attention system for DNA?

You have done no more to show an actual distinction in the approach than TFA and its linked blog post... It sounds like a naming thing to me. On one side we name the term/program as a term and see it as something checked by the kernel, and on the other you name the term/program as a program and see it as something executed by the runtime. What's the difference?

To be fair, lean wastes and leaks memory like a sieve, but this is almost all in the frontend. It has nothing to do with the kernel or the theorem proving approach chosen.

Well... effect programming using vtables. I think this is an emerging paradigm, but it is very early yet so it's difficult to define precisely.

My primary inspiration for the concept is theorem proving languages like Lean in which typeclasses ("interfaces" in the OOP terminology) are implemented using structures passed down as arguments ("vtables" in the OOP terminology) separately from any receivers (values of the type implementing the interface, which doesn't actually need to exist for Lean). Typeclasses (and interfaces) are an effect, albeit a simple and limited one. Lean can't express effects in their generality due to totality requirements, but the same mechanism would work perfectly well for effects too. As for the "vtable" aspect: the primary distinction in implementing typeclasses using exposed vtable passing is that the language does not in any way limit the programmer to zero or one implementations of a typeclass per receiver type(s) (cf. orphan rules in Rust, cf. compiling effect systems to witness-passing, etc.).

No, I'm saying it is checked and then discarded. (Or at least, discarded by the kernel. Presumably it ends up somewhere in the frontend's tactic cache.) That matches perfectly the metaphor, "rubs out earlier parts of proofs to make space for later ones".

The shared misconception seems to be in believing that because _conceptually_ the theory implemented by Lean builds up a massive proof term, that _operationally_ the Lean kernel must also be doing that. This does not follow. (Even the concept is not quite right since Lean4 is not perfectly referentially transparent in the presence of quotients.)

The author appears to have a serious misconception about Lean, which is surprising since he seems to be quite knowledgeable in the area.

Specifically, the author seems to be under the impression that Lean retains proof objects and the final proof to be checked is one massive proof object, with all definitions unfolded: "these massive terms are unnecessary, but are kept anyway" (TFA). This couldn't be further from the truth. Lean implements exactly the same optimization as the author cherishes in LCF; metaphorically, that "The steps of a proof would be performed but not recorded, like a mathematics lecturer using a small blackboard who rubs out earlier parts of proofs to make space for later ones" (quoted by blog post linked from TFA). Once a `theorem` (as opposed to a `def`) is written in Lean4, then the proof object is no longer used. This is not merely an optimization but a critical part of the language: theorems are opaque. If the proof term is not discarded (and I'm not sure it isn't), then this is only for the sake of user observability in the interactive mode; the kernel does not and cannot care what the proof object was.

Deceitful omission from TFA: the warning lights which the firefighter admits seeing override any tower authorization. Omitting this leaves a reader with several incorrect impressions:

INCORRECT: The truck was cleared to cross the runway.

CORRECT: The truck was forbidden to cross the runway due to the active conflict lights.

INCORRECT: Airport safety systems failed.

CORRECT: The only safety system relevant to the crash is the one which would actually alert the truck not to enter the runway, not the one that would alert the controller after the incursion happened (after all, the controller realized immediately what had happened). That system was, by the firefighters' own admission, working perfectly.

INCORRECT: The fault lies mostly with the controller.

CORRECT: While the controller made a bad error which contributed significantly to the accident, nevertheless, the proximal cause of the accident was the truck driver's failure to obey the mandatory direction given by the fully functioning runway safety system.

Zig is just doing vtable-based effect programming. This is the way to go for far more than async, but it also needs aggressive compiler optimization to avoid actual runtime dispatch.

> a version of the Internet that is just intermittently and somewhat mysteriously broken.

That's actually just how the Internet is. Nothing to do with the great firewall.

Yes, absolutely.

You have to throw the context away at that point. I've experienced the same thing and I found that even when I apparently talk Claude into the better version it will silently include as many aspects of the quick fix as it thinks it can get away with.

I've been using pi.dev since December. The only significant change to the harness in that time which affects my usage is the availability of parallel tool calls. Yet Claude models have become unusable in the past month for many of the reasons observed here. Conclusion: it's not the harness.

I tend to agree about the legacy workarounds being actively harmful though. I tried out Zed agent for a while and I was SHOCKED at how bad its edit tool is compared to the search-and-replace tool in pi. I didn't find a single frontier model capable of using it reliably. By forking, it completely decouples models' thinking from their edits and then erases the evidence from their context. Agents ended up believing that a less capable subagent was making editing mistakes.

The far more important question is whether it's bad for the stock price of a few pharma companies.

I mean imputed prestige within the organization. Being an L5 is nothing; it's the promote-or-fire cutoff at Google AFAIK. But being a Principal is slightly more than nothing; it's two levels above the promote-or-fire cutoff.

I mean, _now_, sure, I'd assume Microsoft Principals should be hired around L4 at Google. But that's just due to a temporary inbalance in the decline of legacy organizations. Give it a few years and it will even back out and msft 64 will be in the middle of L5 range like levels.fyi claims.

I've worked at both Microsoft and Google in the past 6 years and the notion that msft "Principal" is equivalent to goog L5 is crazy.

> We won't do something like this again.

This has just as much value as when an LLM claims it won't make a certain mistake again, and for exactly the same reason.

I think about this at least once a week.

I first became aware of the phenomenon of an enlightened anti-UNIX bundle in ZFS; in particular how it unifies lvm, RAID, and the filesystem. While zfs isn't universally loved, it seems that each hot new filesystem that comes out now adopts this strategy as well.

While this doesn't lead to immediate enlightenment about where the balance is, it does highlight an important aspect to consider: whether the whole is more than the sum of its parts. One way openzfs is more than the sum of its parts is that it closes the RAID write hole. The next step, whether it be stabilized in openzfs or otherwise, is to merge encryption into the stack: The current state of the art is to compose block encryption with zfs on top. But a better solution would be for zfs's object layer to encrypt its blocks itself. Because the blocks are not required to have a particular disk alignment or size, the filesystem can offer authenticated encryption without losing the random-access property, as well as granular keys, thus offering some clear advantages over the UNIXy composition method.

Actually I'm not sure how strong an example ripgrep is by comparison. Could a `find` replacement do the ignore patterns just as well? OTOH, does ripgrep offer better I/O and compute parallelism than a naive xargs/parallel?

> This works so much better.

Pi coding agent does this by default with all outputs but Claude (all versions tested, including opus 4.6) just completely ignores this capability. Even when the tool output explicitly tells the agent that the full output is saved in a particular file, Claude reruns the command.