It affects it very heavily IME. People need to make sure they are getting a good mix of writing from other sources.

Yeah, I do not find performances like this very impressive.

What is your attack model here? Each request lives in its own arena allocator, so there is no way for any potentially malicious JavaScript to escape and read memory owned by any other request, even if there is a miscode. otherwise, VM safety is delegated to the V8 core.

Believe it or not, using arenas does not provide free memory safety. You need to statically bound allocations to make sure they don't escape the arena (which is exactly how arenas work in Rust, but not Zig). There are also quite a lot of ways of generating memory unsafe code that aren't just use after free or array-out-of-bounds in a language like Zig, especially in the context of stuff like DOM nodes where one frequently needs to swap out pointers between elements of one type and a different type.

In that blog post, the author said safer than C not Rust.

Yeah people dramatically overestimate the difficulty of getting one's definitions correct for most problems, especially when you are doing an end to end proof rather than just axiomatizing some system. They are still worth looking at carefully, especially for AI-generated proofs where you don't get the immediate feedback that you do as a human when something you expect to be hard goes through easily, but contrary to what seems to be popular belief here they are generally much easier to verify than the corresponding proof (in the case of formally verified software, the corresponding analogy is verifying that the spec is what you want vs. verifying that the program matches the spec; the former is generally much easier).

This website made me suddenly have a huge feeling of loss for what the web could be like. It is so snappy (in the way old static sites could be) but without the page transitions that made them fall out of fashion.

> if you spend too much time interacting with LLMs, you eventually resemble one

Pretty much. I think people who care about reducing their children's exposure to screen time should probably take care to do the same for themselves wrt LLMs.

It makes people uncomfortable. That's the long and the short of it.

Yeah this is something I think a lot of people tend to overlook. People are far too quick to rewrite "we don't know of any reason why it would be impossible" to "we know how to do it" in their heads.

I've done a bunch of theoretical PL work and I find this to be a very surprising result... historically the assumption has been that you need deeply "non-computational" classical axioms to work with the sorts of infinites described in the article. There was no fundamental reason that you could give a nice computational description of measure theory just because certain kinds of much better-behaved infinities map naturally to programs. In fact IIRC measure theory was one of the go to examples for a while of something that really needed classical set theory (specifically, the axiom of choice) and couldn't be handled nicely otherwise.

Much of your comment seems to be about your culture — eg, assuming things about axioms and weighting different heuristics. That we prioritize different heuristics and assumptions explains why I don’t find it surprising, but you do.

From my vantage, there’s two strains that make such discoveries unsurprising:

- Curry-Howard generally seems to map “nice” to “nice”, at least in the cases I’ve dealt with;

- modern mathematics is all about finding such congruences between domains (eg, category theory) and we seem to find ways to embed theories all over; to the point where my personal hunch is that we’re vastly underestimating the “elephant problem”, in which having started exploring the elephant in different places, we struggle to see we’re exploring the same object.

Neither of those is a technical argument, but I hope it helps understand why I’d be coming to the question from a different perspective and hence different level of surprise.

The reason people had these assumptions is because people have been trying (unsuccessfully) to find a constructive interpretation of this stuff for a very long time. Even very fundamental results in measure theory like the Heine-Borel theorem typically require some extension to traditional constructive axioms. Like I absolutely get where you are coming from, but there are a large number of "nice" classical results that definitely do not have constructive counterparts. It's cool that descriptive set theory is not one of them but it's not obvious by any stretch of the imagination, and the pattern you're using to say that it's probably true ("Curry Howard maps nice to nice") is not great process IMO since it would fail in a lot of other cases.

This is the quality of discourse I expect at this point from anti-Rust folks, yes.