_flux

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.

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.

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").

Rust-Brotli (by Dropbox) is actually a drop-in replacement for the Brotli C lib: https://github.com/dropbox/rust-brotli#:~:text=rust-brotli%2...

Dropbox switched to it a decade ago, so it's probably quite product-ready.

I can understand why people used a C library for these apps, as when HTTP2 was specified, the C lib was the only game in down.

However, why not switch to the Rust lib when it was available? I suppose people at Dropbox are now pretty happy they did in 2016: https://dropbox.tech/infrastructure/lossless-compression-wit...

It's slower, though. Too high a price to pay for safety it seems.

Why is it a bad analogy? I don't have experience on either of the libraries, so I may be missing something.

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.

Maybe we should start with something easy and clone Nethack by just playing it through..

Astra Max can do 12%: https://balrogai.com/

Though after improving the harness it can fare better, but still no completion: https://roger-creus.github.io/blog/astra-craftax-nethack/

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.

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.

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.

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

I don't use Claude, but it appears it is permitted to use Claude as a stdin/stdout -communicated tool using JSON, or use Claude SDK, with the monthly plans. Monthly Max/Team plans also include credits that could be used directly via the API: https://support.claude.com/en/articles/17154008-monthly-api-... .

E.g. OpenCode can be used with all three methods. Looks like it needs a plugin for the two Claude methods, though.

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.

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.

Is it possible to implement a very good mechanism?

In similar fashion in the Android Play Store they moved the search off from the top bar. For some time they educated users that "oo the search is no longer here, you need to click there -> to get to the page with search!". That has stopped (for me?), but they still haven't found any other use for same place in the first view.

I suppose it was too convenient.

You mean the article in general is 100% LLM, or the arrangement of these four words is 100% LLM?

I find it extremely unlikely LLMs would have the monopoly on this particular word arrangement—and indeed they would have learned it from training material produced by people in the first place.

I used TLA+ in a (hobby) web app by asking it to model the endpoints and the data user can get from them, and then what kind of access that data can grant in the system, and then implement some properties over that kind of data. I suppose basically like "you can't get access to another user's shopping basket", although mine was maybe a bit more convoluted.

These probabilistic guessing machines are pretty great for creating these formal models, e.g. TLA+, and then guessing if the implementation aligns with the spec.. In fact, it's my go-to tool for constructing soft guardrails for the model, so the design it's going to implement is logically sound. Same as for people: it's easier to make something working when you have a spec that is working.

Of course, it still allows the risk that you don't actually get to understand it.

Let's say we have removed all elements from the hash. Then all following contains -calls will need to be O(n), if I understood correctly? They need to check every slot in the array to confirm inexistence, rather than just one bucket.

The standard hash table has buckets, though, not just a single array that is probed through in case there's no space for a value in the slot determined by the hash function?

This isn't great though if you need to find out if an element exists in the table, and you have the ability to remove elements from it. I suppose you could optimize the hash table after deletions, but that again would be slow.. ?

Btw, this reminds me a bit of Cuckoo hashes. Never used them but seems like a nice idea.

I think the key here is that split view makes one tab show two sites. So when you switch the tab, you switch both views at the same time. You can't achieve this with a window manager, unless you already (instead of tabs) used only windows that your window manager rendered as tabs, and then comes also with this feature. Does any?

I believe Matrix does solve this, at least to an extent.

> Go channels aren't unique, because by the time Go came around pretty much every primitive had been tried somewhere, but it is to my knowledge the only langauge that lifted channels up into the language itself and made them first class.

Concurrent ML had something like that, and it was implemented in OCaml as well: https://ocaml.org/manual/5.5/api/Event.html

And I would say it even goes further than Go by making the actual events first class (no need for language support for this either): send, write and choose (aka select) are also events, so you can build your own things you can select on. Select would be basically defined as

    let select events = sync (choose events)

so sync is the way to convert events to values (and blocking in the progress).

CML had one extra trick in its sleeve: it was able to garbage collect threads that were not able to proceed. I'm not aware of any other system that can do that. This would e.g. resolve leaking coroutines in Go, at least in some situations..

With this cost, does it perform the same quality and speed as Jev?

I'm quite interested in this; my current understanding is though that Jev is great when scored with response quality and latency metrics.

So actually the answer to your question is that Rust provides excellent guardrails against memory safety issues, and in some cases, for code correctness as well, by allowing more behavior to be encoded in types. One of those guardrails is borrow checker.

Thus, the agent needs to iterate less.

I expect a real big-gish project would have possibly hundreds or thousands of such sessions. And personally I've never needed to dig back an old session for reference, only when I'm still actively working on the topic. They don't have a particular structure, whereas the actual code has a lot of structure.

But maybe it would be useful to have the related chats in the actual git commits that introduce the features. This way, if you (or the agent) `git bisect`s an issue, the same context that was used to construct the feature could be used for making the fix as well. I have never tried this approach, but it sounds like it could be useful.

It's slightly annoying that most (all?) harnesses store the chat logs in a db outside the project, and additionally e.g. OpenCode doesn't give the agent a direct way to access the complete current session context. So implementing this currently would be a bit hacky (find session by time? generate random string in context and find the session?).

> Debian is still easier to manage than RH based systems, and .deb is a really good package manager, and is arguably more sophisticated than RPM.

I realize I'm veering a bit off-topic :), but I've used Debian for a long while, but I do wonder how is that deb is more sophisticated than rpm?

The one feature I remember (a long time ago) rpm being able to install the different versions of the same package, although I suppose this in practice would only work for packages made for this, and libraries would usually be such packages. With debs this means the version number needs to be embedded to the package name with some developer-chosen precision.