> How much of the identity of a mathematician is tied up in being the first to discovery?
Here is how I'd put it: math has an enormous focus on discovery. It is why we have Godel's incompleteness theorems, the Cantor set, Zorn's lemma, and so forth. We name things after their discoverers.
It is possible that, going forward, no more things will be named after human discoverers. The last such naming (of something truly significant) may already have occurred.
That is a massive culture change, at the very least.
> We reuse WebAssembly linear memories under the covers to implement and sandbox the GC heap. A reference to a GC object is not a native pointer, it is a 32-bit index into the GC heap’s underlying linear memory [..] As far as being fast goes, it lets us use virtual-memory guard pages to elide explicit bounds checks, just like we do for linear memories
Array loads and stores still need an explicit bounds check, don't they? And struct loads and stores don't have one anyhow. Are there other bounds checks that Wasmtime is removing? I can't figure out what they mean here.
Yes, formal mathematics has such limits. We can't expect machines to be perfect and provably perfect. But the industry isn't assuming that. Why would it? Natural intelligence is not perfect or provably perfect, either.
Rather than certainty, measurement is often enough. We can't prove a program will always halt, but we can check it halts in a specific execution.
Approximation is also often all we need. Even if we can't prove that we can train a network with more than 50% success, if we can get multiple shots at that (using different data, or initial random weights, or training techniques, or something else), then we can reduce that danger exponentially. (I don't know that we have a guarantee of succeeding there, but this would be the hope, and I am not aware of anything showing it is impossible, unlike perfect provability.)
Finally, it is possible that perfect provability does work on the problems we care about. Godel and Turing etc.'s proofs rely on finding rare situations where we can't prove things - cleverly-constructed pathological cases - but perhaps human behavior does not fall into that set. Human behavior may not be a pathological case for proofs or learnability.
I'm not sure what "branch on undefined values" means there, yeah, but never reusing memory addresses is enough to prevent use-after-free.
Or, rather, you can use a value after freeing it, but it will not be exploitable, because it will contain valid data of the right type. This is the same idea as Type-After-Type,
> The Zig standard library also has a general-purpose debug allocator. This is a safe allocator that can prevent double-free, use-after-free and can detect leaks.
I don't know if that allocator is Zig's default or not in that compiler mode, but it could be. Solving temporal memory safety in general is something we know how to do, the only issue is the overhead, see e.g. Type-After-Type
They made a claim about language models in general, not just ones that had been released so far.
The point of the paper, in fact, is that language models are getting "too big", and another approach is needed to make progress, so they were certainly predicting things about later models.
With that said, they talked about "pure" language models, so it is fair to say that they didn't talk about, say, LLMs that are multimodal or that have tool use, which are advances that happened after their paper.
My main criticism of the paper is that it says LLMs work "haphazardly", using probabilistic information. That is a hypothesis, but it is stated as a known fact, a fundamental limitation.
It is true that LLMs often behave haphazardly, and do rely on statistics. But plenty of research has shown them behaving in methodical ways too. There are findings going both ways!
Granted, many of the strongest contradictory results appeared after the Stochastic Parrots paper, so it isn't like they were ignoring the literature at the time. But they did make a very strong claim, and in the half-decade since, a lot of evidence has come out against it.
Note that wasm is still lean and fast - WASI is not part of core wasm, but layered on top.
That is, it is possible to implement wasm without WASI. That is also true for other wasm proposals like WasmGC. It is very possible that parts of the ecosystem will not implement certain proposals if they don't make sense there (e.g. parts of the embedded ecosystem may never add GC, etc.).
> I believe that artificial intelligence has three quarters to prove itself before the apocalypse comes, and when it does, it will be that much worse, savaging the revenues of the biggest companies in tech. Once usage drops, so will the remarkable amounts of revenue that have flowed into big tech, and so will acres of data centers sit unused, the cloud equivalent of the massive overhiring we saw in post-lockdown Silicon Valley.
We have seen 8 quarters since. Has any of that come to pass?
> Suppose one copies an LLM into AoE II and feeds into the AoE II-LLM ‘I feel lonely’ as an input. This AoE II-LLM replies: ‘I feel bad for you, maybe catch up with a friend? Closeness always helps in these situations’. One would be hard-pressed to make a convincing argument that, because of this response, an AoE II-LLM knows what helps in these situations
I don't see why one would be any more hard-pressed to make that conclusion about this system than a "normal" LLM.
That it is harder to "read" the data out is the only difference (the AoE II-LLM's output is encoded in game elements). But is ease of decoding an actual issue? If we can't understand a group of people that speak another language, does that say anything about them, or about us?
Here is how I'd put it: math has an enormous focus on discovery. It is why we have Godel's incompleteness theorems, the Cantor set, Zorn's lemma, and so forth. We name things after their discoverers.
It is possible that, going forward, no more things will be named after human discoverers. The last such naming (of something truly significant) may already have occurred.
That is a massive culture change, at the very least.