Rochus

Interesting, thanks. So you need a Node based server to run it.

Interesting. But what is actually the "unique selling point" compared to Harfbuzz? The "single file" implementation? The size?

Cool. How do you have implemented the latex rendering? Are you using one of the common libraries? Is the rendering (incl. PDF etc.) directly running in the browser, or on the server?

> the guy who played the CD 50 times would today need to stream it... 50 times. In a standard record deal, the number is much higher than 50. Usually, the artist only keeps $0.0006 per song (15% …

> I knew they did it for their own pleasure. The shepherd can afford to sing for hours because he has a job herding sheep. The modern musician, by contrast, is often told to "get a real job&…

> Connection Became Commodified ... Music is now background noise It's rather the music itself which became a commodity, and it's not mainly background noise, but is reduced to a functi…

Claiming someone explains capitalism "better than Marx" is a low bar. It is widely accepted that most of Marx’s central predictions did not materialize as he forecasted, not even during his …

I was looking for information about Xous's raw IPC performance to get an impression of how it performs compared to e.g. the L4 family, especially L4re and sel4. Also a comparison to QNX would be …

Thanks for the hint. Just tried Mixea and the results sounds surprisingly good. Here is what I got without any adjustments: - original: http://rochus-keller.ch/suno_2025_2/suno_Es…

The mastering is amazing; it sounds much better than what the Suno built-in mastering can do (I even hear less of the typical Suno artifacts); can you share what AI mastering you are using?

I like those kinds of comparisons where you also can hear a part of the song directly, even if only a few seconds. The actual "advantage" of the present songs I noticed in the video is, that…

It's "proven correct" (i.e. verified) if the backtranslation renders the same intent as the original. That's the whole purpose of the idea.

Thanks, that's exactly what I was asking about. So if I understand correctly: for the hardware interface layer (DMA, MMIO), you're essentially writing disciplined C-style code in unsafe bloc…

Thanks, interesting. My concern was less about which language implements std, but rather about the semantic mismatch between Rust's ownership model and hardware behavior (e.g. DMA aliasing, MMIO …

Are you one of the authors? Concerning the "infrastructure": Rust assumes a runtime, the standard library assumes a stack exists, a heap exists, and that main() is called by an OS; in a kern…

Great, thanks. I assume the "kernel" makes heavy use of "unsafe", because all the infrastructure assumed by Rust is not available. Or how was this solved?

What are "Jazz Translations"? Has there been an audio original which was uploaded, or were there overdups over the Suno track, or additional mastering? It sounds better (both musically and a…

My bet is that AI changes the economics of that verbosity, making it cheap to generate and check those 'huge' definitions layer by layer. The next four years will show.

I think there is a misunderstanding about what is being back-translated. We don't back-translate the proof steps (the thousands of intermediate logical derivations). That would indeed be verbose …

We build pretty complex systems only based on "natural language" specifications. I think you are conflating specification ambiguity with verification accessibility. > What does one gain …

Interesting, didn't hear from this system so far. Seems to be funded by the EU. Apparently it is written in pure Rust since 2020, and Andrew "bunnie" Huang seems to be involved. Is ther…

> you are writing a post that does that about a different technology No, I report based on my experiments and realistic expectations. I don't promise: "just rewrite in Rust and everything…

Interesting article, thanks. There is indeed a "semantic gap". However, there is also a practical solution: bidirectional LLM translation. You can verify the formal specification by back-tra…

As a senior engineer, I am quite alienated by the hype and the completely exaggerated promises that are being made to people. It is precisely such exaggerations that inevitably lead to equally exagger…

That was deliberately just a simple example to give people an impression how the "code" looks which the LLM generates. There is no doubt that you can implement a traffic light with a "t…

This is amazing. Where does he find all the time?

Life as a whole is not safe, and not everyone seems to be aware of this.