Recent submissions

Comment · 2 days ago
Fun to embed m4a files that could just do this all by themselves?-)

I think the most disappointing thing about these is that you cannot quite record over them (over zip files) in real time, unless you arrange the particular m4a files to be wavs with e.g. PCM or A-law, or I suppose some more sophisticated but constant bitrate codec, and then also arrange that file to be uncompressed in the zip.. ? I doubt there are libraries to help make that happen?

At least if they were just plain mpeg4 containers, the reduced amount of indirection would make the problem a bit easier and could probably be manipulated with GPAC/MP4Box almost just as easily as zip files.

Comment · 3 days ago
It might be bit of an effort to get Fil-C compiling the Linux kernel. As I understand it, it would amount to running garbage collector in the kernel, so some care would probably need to be taken to ensure it doesn't stop things at the wrong time, e.g. interrupts.
Comment · 9 days ago
Why should it?

I believe though it is an old phenomenom that if (given the default context) you ask a random number, it will more often than not give numbers from a very small set.

I just used a "Temporary chat" with ChatGPT twice to "Give a random number" and it gave 42 both times (this shuold be rather understandable why it ended up with this). Then I asked "Give a random number in 1-10" twice and it responded with 7 for both (and this too is an old "magic number").

Comment · 10 days ago
Comment · 10 days ago
Comment · 16 days ago
Why is it a bad analogy? I don't have experience on either of the libraries, so I may be missing something.
Comment · 20 days ago
I would say as stated there were two ways to read the claim:

- either that the claims are paired as you say (the second one implying that the program cannot be fixed),

- or that the claims are completely distinct, that simply state the desirable state of things.

Using the second interpretation, the corollaries would be:

- there is (typically) no reasonable fix for the C++ compiler that would address the UB. Therefore to fix the UB all C++ programs exhibiting the same need to be fixed, which is hard, as the compiler will keep accepting them.

- once the Rust compiler is fixed, then all safe Rust programs exploiting the bug must now be fixed, or the compiler will reject them.

What I would sign under would be the second interpretation, not the first one. But I intentionally also selected the particular ambiguous form due to the cutesy, albeit misleading, symmetry of the statements.

Comment · 20 days ago
Comment · 20 days ago
I suggest you point the exact statement where I claimed the corresponding safe Rust program is impossible to fix to avoid unsound behavior.

I hold the argument that if the Rust compiler produces unsound behavior for safe Rust, then the compiler needs to be fixed.

Comment · 20 days ago
I don't find that anyone made a claim that the program could not be fixed. Why are you suggesting to find a proof of this?

The point of course was not that what you can do, but what you should do. All cases of safe Rust compiler producing unsound code should be fixed, but the same argument is more difficult to make for C++.

Sometimes should might be different of what you must. For example, if your program exhibits unsound behavior in safe Rust (or C++) code, it's probably a lot more practical to just change the program so that it doesn't, instead of updating the compiler, unless you happen to be a Rust compiler developer. But, at the same time, you should file an issue about it.

You can of course find C++ compiler bugs as well, although I expect that to be quite rare nowadays. But the typical case is that if a C++ program exhibits unsound behavior, there is no reasonable compiler fix for it.

Then there's of course Fil-C! This improves the situation greatly by converting most interesting cases of unsound behavior into runtime errors. It seems not everyone is happy with the runtime costs of making this happen, though. And you must compile everything with Fil-C. It doesn't work with Windows or MacOS either.

Comment · 21 days ago
Sure, usually the program can be changed to avoid the issue, but the key here is that the Rust compiler is wrong and needs to be fixed. Once fixed, the actual program fix also falls in place, as it cannot be compiled anymore.
Comment · 21 days ago
I think the difference is here:

- If a compiled C++ program has unsound behavior, the program needs to be fixed

- If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

Comment · 21 days ago
Comment · 25 days ago
Hmm, so actually I thought it would say that it's not permitted to benchmark or compare to other products, but I can't find such claim?

It does say "develop (or to facilitate the development of) a similar or competing product or service", but I think it would be a long stretch to say that's the case if they would just publish benchmarks. Microsoft legal department might disagree.

Comment · 27 days ago
Actually, as an earlier commenter noticed, it seems that the proof was done in natural language, and only then translated to Lean, as https://openai.com/index/navier-stokes-solution/ says:

> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

So it suggests that the formalization/verification step may have fixed some issues in the natural language proof, and either such differences were never noticed or the corrections weren't ported back to the NLP.

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton