Earlier quoted context omitted.
You're being needlessly dismissive. From a philosophical perspective, there's no way to know that any piece of software is truly correct without formal verification. But in the present, non-philosophical context, it's obvious that what we mean is, colloquially, "how well-tested is this against a variety of edge-case files which the official winrar handles correctly? Is there a test suite, and how robust is it? Plenty…
The post mentions the existence of an extensive test suite, which you can peruse for yourself if you're so inclined: https://github.com/bitplane/rars/tree/master/crates/rars-for... I don't know how all these test cases were generated, but at least some of them seem to have been copied (with attribution) from the test suites of earlier FOSS RAR implementations. The ideal would be to test it against a representative co…
Rars: a Rust RAR implementation, mostly written by LLMs
61–70 of 92 posts
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#62Earlier quoted context omitted.
I added the second paragraph about formal verification at the same time you posted, in anticipation that you'd immediately dig your heels into it otherwise, despite me highlighting that the other methods are merely empirical. I was immediately proven right once I pressed "update". That said, I have now deleted my snarky response that followed. Not in the game of capitalizing off of the human equivalent of a race cond…
Haha, off course! The three major sources of software failures: off by one errors and race conditions.
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#63Earlier quoted context omitted.
Thus all software that can be used is correct? You know what I meant: How can we have confidence that this implementation of RAR is functionally identical to what it's based on? What would give me the confidence to use it in a critical piece of infrastructure?
> Thus all software that can be used is correct? You also know what I meant, since I spelled it out in more detail a comment later. But even though you're being facetious, yes, that really is the case. If it works it works. That's the bar for the vast, vast majority of software, and has been since forever. Demonstrated practical correctness. If you stumble into a bug, you log it as a defect and then either wait for a…
I get that this is often the case, but it does feel like we should be able to do better. At least when humans write this code you can have the expectation that there was real intent behind making sure the semantics of the code are aligned with the specification. At least with current language models, they tend to just brute-force test suite acceptance until everything passes, in a way no human developer has the capacity for. Of course this is often how it works with humans too (i.e. the classic Oracle story), but it does feel wrong.
Can we be sure that this method has produced a correct artefact without years of extensive usage? Probably not, hence my reluctance to rely on something like this, at least initially.
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#64Rar is proprietary. Good luck.
https://law.stackexchange.com/a/83552 I suppose the question is whether the author had ever entered into a contract limiting reverse engineering...
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#65Earlier quoted context omitted.
The point is, excepting current legal standards which are already very murky, how can _you_ claim copyright, if you don't _know_ it isn't encumbered? You can get these LLMs to generate copyrighted outputs both intentionally and accidentally. This is a known fact; therefore, if you're not checking the output to see if this has occurred then you're potentially generating legal risks for yourself and anyone who uses you…
What do you mean by "checking the output"? Is there some kind of check the author says he didn't do that you think he should have? Or is your claim that using an LLM for coding is always copyright infringement? If so, I think the risk that I'll personally be the test case that resolves whatever ambiguities exist in the law is basically zero, and I don't think derailing the thread to be about that topic enlightens any…
At the very least you could see if it's already been open sourced under a different license. If you take GPL code and just slap MIT on it do you not consider that a violation?
> Or is your claim that using an LLM for coding is always copyright infringement?
I'm claiming you cannot really know.
> I'll personally be
It may be someone who uses or redistributes your code in any fashion.
> derailing the thread
I've made two posts. One with an idea and the second clarifying it. This is not "derailing the thread" under any sane definition. This is simply a complicated and relatively unexplored topic that clearly draws a lot of interest and resulting conversation from the crowd here.
I think using this type of bullying rhetoric damages that conversation and harms the reputation of Hacker News in general and I always regret it when I see it.
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#66> But, it works, and the world now has a free software RAR implementation. Does it? How are you legally intending to use copyright to license this machine output? How would you know it's not encumbered in any way?
In all seriousness, why should anyone care? I always found software IP to be absurd, but this is a particularly absurd situation. We're talking here about a small utility tool implemented from scratch and open sourced, with no apparent intent to make any money from it. Are you concerned about the "encumberence" of using "unlicensed" tools to manipulate .doc, or .pdf, or .mp3 files?! Well I'm not, and if anyone ever t…
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#67Earlier quoted context omitted.
Really unsure why this is getting downvoted, to my understanding this is a massive, unsettled concern. It wasn't even a disasm/pseudocode to formal spec flow, and then a separate human implementation. The same human has been in the loop throughout, and large parts of it were generated directly. It's basically guaranteed tainted. Edit: I should have skimmed a bit more patiently, there was in fact no "disasm/pseudocode…
I read the post you're replying to as saying "this is copyright-encumbered and nonfree because it's a derivative work of everything in Claude's and GPT-5.5's training corpus", which is an argument I find fairly tiresome. (Realistically, if courts actually rule that this is the case, this tiny little project will be the least of anyone's concerns.) "This is copyright-encumbered and nonfree because it's a derivative wo…
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#68Earlier quoted context omitted.
> Thus all software that can be used is correct? You also know what I meant, since I spelled it out in more detail a comment later. But even though you're being facetious, yes, that really is the case. If it works it works. That's the bar for the vast, vast majority of software, and has been since forever. Demonstrated practical correctness. If you stumble into a bug, you log it as a defect and then either wait for a…
> You just do a bunch of empirical testing and hope for the best. I get that this is often the case, but it does feel like we should be able to do better. At least when humans write this code you can have the expectation that there was real intent behind making sure the semantics of the code are aligned with the specification. At least with current language models, they tend to just brute-force test suite acceptance…
There's a lot of chatter lately e.g. about using TLA+ for formal modeling, so that anything downstream can be formally proven. That helps, but then the formal model still needs to be crafted somehow, which means a pass of semantic interpretation.
Going from binary to spec mechanistically via formal proofs would be possible, but only if there was a formal spec for the binary structure and the ISA available. In practice, both are just natural language prose too however, meaning another interpretation pass or two. The ISA specs also keep a lot implementation-defined / undefined afaik, for microarchitecture-level optimization freedom.
Netlists, PDK, and the likes then might be public for some RISC-V designs these days, but to get the actual chip behavior requires EM simulation typically on a scale that is not possible for any chip performant enough to be of interest. And RISC-V is not a very broadly adopted platform for proprietary consumer software.
Having the human do the semantic mapping is expensive and legally stricken. Having an LLM do it is more risk, but way, way, cheaper and currently legally grey. And both can and do make mistakes.
This is why I see this so bleakly. That said, I do also think formats like this are delicate enough that even rudimentary empirical testing should provide a surprisingly decent behavioral coverage. There's a reason that "I can't believe anything ever works at all" is such a common sentiment. Practical usage is a surprisingly powerful gate, and fuzzing in particular is basically that on steroids.
I do nevertheless still secretly get the heebie-jeebies from the Linux NTFS implementation though (me bringing that up was no coincidence).
Re: Rars: a Rust RAR implementation, mostly written by LLMs
#69Earlier quoted context omitted.
I mean, not really...? A vibecoded mess that runs badly, that's not really the hard part for something like compression/decompression tools.
What's your easy way of reverse engineering every previous version of this file format, if you don't think that was the hard part?
Still, OP claims to have done the best job to date at creating (via AI) specs, and the non-optimal Rust implementation, so a net gain?