Rochus

15 ms·

331.
by Rochus 9mo ago
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 after the few seconds I pretty well kno
332.
by Rochus 9mo ago
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.
333.
by Rochus 9mo ago
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 blocks with volatile reads and manual memory
334.
by Rochus 9mo ago
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 side effects). So I was curious what wor
335.
by Rochus 9mo ago
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 kernel, none of this is true. And the borrow
336.
by Rochus 9mo ago
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?
337.
by Rochus 9mo ago
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 also the sound quality) than what Suno v5
338.
by Rochus 9mo ago
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.
339.
by Rochus 9mo ago
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 and useless. We back-translate the speci
340.
by Rochus 9mo ago
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 besides familiarity by translation back
341.
by Rochus 9mo ago
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 there a PDF version of the book ( https:&#x2
342.
by Rochus 9mo ago
> 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 is safe, and don't hesitate to spe
343.
by Rochus 9mo ago
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-translating it to natural language with ano
344.
by Rochus 9mo ago
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 exaggerated counter-movements (such as today&#x
345.
by Rochus 9mo ago
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 "traditional" programming approach. T
346.
Why Rust solves a Problem we no longer have – use AI and Formal Proofs instead(rochuskeller.substack.com)
8 points by Rochus 9mo ago|7 comments
347.
by Rochus 9mo ago
This is amazing. Where does he find all the time?
348.
by Rochus 9mo ago
Life as a whole is not safe, and not everyone seems to be aware of this.
349.
by Rochus 9mo ago
> They should rewrite it in Rust. Why they? You should do it.
350.
by Rochus 9mo ago
Rather remove the downvote function completely, because it is mostly misused and stimulates the "lower instincts" of people.
351.
by Rochus 9mo ago
Better? I made a few posts about my work some years ago an met significantly more naggers and nitpickers than on HN; I didn't see a downvote function (in contrast to the author of the article), but flagging was obviously misused a lot.
352.
by Rochus 9mo ago
The report finds that the global music copyright business generated $47.2 billion in 2024, representing a 5.2% growth from the previous year, though this growth is slowing compared to the post-pandemic boom. For the first time in years, pub
353.
by Rochus 9mo ago
Looks like a substantive and novel contribution to symbolic music generation. Its significance lies in bridging Dmitri Tymoczko’s very recent music theory with rigorous functional programming patterns. The article describes a Generative Gra
354.
by Rochus 9mo ago
Just wanted to say that I skipped LuaTex 1.10 because not even a bare Hello World worked. So I switched to LuaTex 1.18 including the HarfBuzz library. I even implemented my own OTF loader in C (with Lua bindings for additional required Harf
355.
by Rochus 9mo ago
I now have migrated LuaTex 1.10 and also 1.18 (with HarfBuzz) to my BUSY build system assuming that at least with the latter I could get rid of any TexLive dependency (especially the luaotfloader). I even implemented my own OTF loader in C
356.
by Rochus 10mo ago
This is an interesting service. The audio quality seems similar to Suno 4.5, and the "creativity" and "musicality" is pretty good as well. Here are two tracks I was able to generate (download was only possible via networ
357.
by Rochus 10mo ago
The major Swiss media outlets (SRF, Tages-Anzeiger, Blick, Watson) have reported on this, but mostly under headlines that classify Baud as a propagator of propaganda or conspiracy theories (e.g., SRF: “Russia's mouthpiece,” Blick: “Bet
358.
by Rochus 10mo ago
Great that this lecture (series) was recorded and we are able to watch it today! Thanks for sharing.
359.
by Rochus 10mo ago
Ok, I see. Raymond wrote this in 2003, at the peak height of "Java OO madness" where deep inheritance and over-engineered, totally inefficient systems were common. In The Art of Unix Programming, Raymond clarifies that he isn&#x27
360.
by Rochus 10mo ago
That's an interesting presentation and a great project. I wasn't aware how many distinctive design concepts are present in this database. That's impressive. Hope I will find time in the new year to use it in a project.

More ›