3 ms·

By using it.

by perching_aix 5mo ago

By using it.

repelsteeltje 5mo ago
It works == it's correct?
- mjr00 5mo ago
  This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct.
  - speedgoose 5mo ago
    use std::fs::File; use std::io::prelude::*; fn main() -> std::io::Result<()> { let mut file = File::create("content.txt")?; file.write_all(b"3!")?; Ok(()) }
    - rakel_rakel 5mo ago
      ; cat content.txt 3!;
  - dataflow 5mo ago
    > This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct. No, it doesn't even need to compile. The mere fact that it's in Rust means it's correct.
- perching_aix 5mo ago
  Yes? What do you think fuzzing, unit testing, integration testing is for? It's an empirical evaluation of correctness. Literally just try and see. For actual correctness verification in the strong sense, you'd need to start from a specification written in a formal language so that it's machine checkable, which if I had to guess not even win.rar GmbH has.
  - repelsteeltje 5mo ago
    I hope the developers of, say, the brakes in my car don't interpret 'software correctness' the way you do. Added, later: hey you changed your comment, added a whole paragraph.
    - deleted 5mo ago
      [deleted]
    - atiedebee 5mo ago
      I hope the brakes in my car don't need developers
      - pixl97 5mo ago
        I think you underestimate the complexity of modern braking systems.
      - arcticbull 5mo ago
        ABS doesn't just appear organically.
    - throw1234567891 5mo ago
      They used to. Now they have systems, standards, and experience. There are only so many ways you can do brakes on the car.
    - perching_aix 5mo ago
      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 condition. I should make a browser addon to delay posting, this is the 2nd time this happens in the past few days. Edit: Nevermind, it's already a feature built into the site. Turned it on. I wonder if it applies to edits also... Nope, doesn't seem to. Oh well, should still help.
slopinthebag 5mo ago
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?
- jaggederest 5mo ago
  Validating compression systems is usually really straightforward. There are 3 layers - decode known values from compressed files (or encode, same), round trip without any alterations, and fuzzing with arbitrary binaries Because it's a defined format there can be binary exact comparisons between the input and output files - we already have an oracle in the form of proper RAR format software, so if they are identical, you don't need to look further for that specific case. You can see a version of this that I did quite similarly, for postgresql wire format, here: https://github.com/pgdogdev/pgdog/tree/main/integration/sql https://github.com/pgdogdev/pgdog/tree/main/integration/sql It validates that sql with the same setup, teardown, and test results in perfectly exact compatibility between raw postgresql as the control and various configurations of PgDog, with both the text format and binary format, so ultimately a 6-way multivariate test that should always result in binary-exact results.
  - slopinthebag 5mo ago
    Right, that's very different from "using it" and it's also different from "Have an LLM generate code that compiles".
- perching_aix 5mo ago
  > 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 fix or fix it yourself depending. That's all that regular people ever have. In the case of this project, this was achieved via fuzz testing. It's literally no different to e.g. validating the NTFS driver that ships in the Linux kernel, or validating any other (re)implementation of anything. You just do a bunch of empirical testing and hope for the best. It is also why reimplementations always lag behind, which I'm not suggesting is not a real concern (or that defects wouldn't be). It's just not a gotcha. Hell, I'm 99% sure this is exactly what the actual vendor does too, or at least I sure hope that they do have tests at least. Cause they're sure as shit not using a formally verified compiler toolchain, meaning they definitely don't have a formal proof about whether even the official implementation in itself is correct. Only empirical data at best too.
TacticalCoder 5mo ago
I could be correct but way too slow in edge cases (unlikely with Rust but you never know), leaking temporary files, having security holes, etc. There's much more about correctness of a piece of software than: "produces the same output as the original on x test cases". I'm not saying it's a bad implementation and, if anything, LLMs are much better at translating/porting existing code (and finding bugs) than at writing things unheard of. You're basically saying, if I may make a pun: "rust me bro, it's correct".
- perching_aix 5mo ago
  [dead]
- davidsong 5mo ago
  Yeah the main things are DoS attacks and path traversal issues. I intentionally guarded against these with resource limits and checks, but I can't guarantee that it's safe. I mean, basically anyone who carefully reads it knows more about it than me - you play the AI slot machine at this scale and who knows what prizes you'll win!

By using it.

repelsteeltje 5mo ago

It works == it's correct?

mjr00 5mo ago
This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct.
- speedgoose 5mo ago
  use std::fs::File; use std::io::prelude::*; fn main() -> std::io::Result<()> { let mut file = File::create("content.txt")?; file.write_all(b"3!")?; Ok(()) }
  - rakel_rakel 5mo ago
    ; cat content.txt 3!;
- dataflow 5mo ago
  > This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct. No, it doesn't even need to compile. The mere fact that it's in Rust means it's correct.
perching_aix 5mo ago
Yes? What do you think fuzzing, unit testing, integration testing is for? It's an empirical evaluation of correctness. Literally just try and see. For actual correctness verification in the strong sense, you'd need to start from a specification written in a formal language so that it's machine checkable, which if I had to guess not even win.rar GmbH has.
- repelsteeltje 5mo ago
  I hope the developers of, say, the brakes in my car don't interpret 'software correctness' the way you do. Added, later: hey you changed your comment, added a whole paragraph.
  - deleted 5mo ago
    [deleted]
  - atiedebee 5mo ago
    I hope the brakes in my car don't need developers
    - pixl97 5mo ago
      I think you underestimate the complexity of modern braking systems.
    - arcticbull 5mo ago
      ABS doesn't just appear organically.
  - throw1234567891 5mo ago
    They used to. Now they have systems, standards, and experience. There are only so many ways you can do brakes on the car.
  - perching_aix 5mo ago
    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 condition. I should make a browser addon to delay posting, this is the 2nd time this happens in the past few days. Edit: Nevermind, it's already a feature built into the site. Turned it on. I wonder if it applies to edits also... Nope, doesn't seem to. Oh well, should still help.

slopinthebag 5mo ago

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?

jaggederest 5mo ago
Validating compression systems is usually really straightforward. There are 3 layers - decode known values from compressed files (or encode, same), round trip without any alterations, and fuzzing with arbitrary binaries Because it's a defined format there can be binary exact comparisons between the input and output files - we already have an oracle in the form of proper RAR format software, so if they are identical, you don't need to look further for that specific case. You can see a version of this that I did quite similarly, for postgresql wire format, here: https://github.com/pgdogdev/pgdog/tree/main/integration/sql https://github.com/pgdogdev/pgdog/tree/main/integration/sql It validates that sql with the same setup, teardown, and test results in perfectly exact compatibility between raw postgresql as the control and various configurations of PgDog, with both the text format and binary format, so ultimately a 6-way multivariate test that should always result in binary-exact results.
- slopinthebag 5mo ago
  Right, that's very different from "using it" and it's also different from "Have an LLM generate code that compiles".
perching_aix 5mo ago
> 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 fix or fix it yourself depending. That's all that regular people ever have. In the case of this project, this was achieved via fuzz testing. It's literally no different to e.g. validating the NTFS driver that ships in the Linux kernel, or validating any other (re)implementation of anything. You just do a bunch of empirical testing and hope for the best. It is also why reimplementations always lag behind, which I'm not suggesting is not a real concern (or that defects wouldn't be). It's just not a gotcha. Hell, I'm 99% sure this is exactly what the actual vendor does too, or at least I sure hope that they do have tests at least. Cause they're sure as shit not using a formally verified compiler toolchain, meaning they definitely don't have a formal proof about whether even the official implementation in itself is correct. Only empirical data at best too.

TacticalCoder 5mo ago

I could be correct but way too slow in edge cases (unlikely with Rust but you never know), leaking temporary files, having security holes, etc. There's much more about correctness of a piece of software than: "produces the same output as the original on x test cases". I'm not saying it's a bad implementation and, if anything, LLMs are much better at translating/porting existing code (and finding bugs) than at writing things unheard of. You're basically saying, if I may make a pun: "rust me bro, it's correct".

perching_aix 5mo ago
[dead]
davidsong 5mo ago
Yeah the main things are DoS attacks and path traversal issues. I intentionally guarded against these with resource limits and checks, but I can't guarantee that it's safe. I mean, basically anyone who carefully reads it knows more about it than me - you play the AI slot machine at this scale and who knows what prizes you'll win!