4 ms·

It works == it's correct?

by repelsteeltje 5mo ago

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.
    - repelsteeltje 5mo ago
      Haha, off course! The three major sources of software failures: off by one errors and race conditions.
- wavemode 5mo ago
  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 of software that claims to be compatible with the rar format, doesn't actually successfully read all rar files." It's also equally obvious, in the present context, that we would prefer these steps to have been taken by the author of the software before we install it and run it on our own computers and data. The parent commenter wasn't just asking about the software's correctness for the sake of academic curiosity.
  - ameliaquining 5mo ago
    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-format/tests 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 corpus of real-world legacy RAR files, but I'm not sure where you'd find one.
    - fragmede 5mo ago
      pirate bay

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.
  - repelsteeltje 5mo ago
    Haha, off course! The three major sources of software failures: off by one errors and race conditions.
wavemode 5mo ago
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 of software that claims to be compatible with the rar format, doesn't actually successfully read all rar files." It's also equally obvious, in the present context, that we would prefer these steps to have been taken by the author of the software before we install it and run it on our own computers and data. The parent commenter wasn't just asking about the software's correctness for the sake of academic curiosity.
- ameliaquining 5mo ago
  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-format/tests 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 corpus of real-world legacy RAR files, but I'm not sure where you'd find one.
  - fragmede 5mo ago
    pirate bay