4 ms·

> The refusal to accept code that the developer knows is correct, How do you know it is correct? Did you prove it with pre-condition, invariants and post-condi

by Ygg2 2y ago

> The refusal to accept code that the developer knows is correct, How do you know it is correct? Did you prove it with pre-condition, invariants and post-condition? Or did you assume based on prior experience.

yohannesk 2y ago
Writing correct code did not start after the introduction of the rust programming language
- Ygg2 2y ago
  Nope, but claims of knowing to write correct code (especially C code) without borrow checker sure did spike with its introduction. Hence, my question. How do you know you haven't been writing unsafe code for years, when C unsafe guidelines have like 200 entries[1]. [1]https://www.dii.uchile.cl/~daespino/files/Iso_C_1999_definition.pdf https://www.dii.uchile.cl/~daespino/files/Iso_C_1999_definit... (Annex J.2 page 490)
  - int_19h 2y ago
    It's not difficult to write a provably correct implementation of doubly linked list in C, but it is very painful to do in Rust because the borrow checker really hates this kind of mutually referential objects.
    - Ygg2 2y ago
      Hard part of writing actually provable code isn't the code. It's the proof. What are invariants of double linked list that guarantee safety? Writing provable anything is hard because it forces you to think carefully about that. You can no longer reason by going into flow mode, letting fast and incorrect part of the brain take over.
edflsafoiewq 2y ago
One example is a function call that doesn't compile, but will if you inline the function body. Compilation is prevented only by the insufficient expressiveness of the function signature.
lelanthran 2y ago
Rust prevents classes of bugs by preventing specific patterns. This means it rejects, by definition alone, bug-free code because that bug free code uses a pattern that is not acceptable. IOW, while Rust rejects code with bugs, it also rejects code without bugs. It's part of the deal when choosing Rust, and people who choose Rust know this upfront and are okay with it.
- bigstrat2003 2y ago
  > This means it rejects, by definition alone, bug-free code because that bug free code uses a pattern that is not acceptable. That is not true by definition alone. It is only true if you add the corollary that the patterns which rustc prevents are sometimes bug-free code.
  - lelanthran 2y ago
    > That is not true by definition alone. It is only true if you add the corollary that the patterns which rustc prevents are sometimes bug-free code. That corollary is only required in the cases that a pattern is unable to produce bug-free code. In practice, there isn't a pattern that reliably, 100% of the time and deterministically produces a bug.

by Ygg2 2y ago

yohannesk 2y ago

Writing correct code did not start after the introduction of the rust programming language

Ygg2 2y ago
Nope, but claims of knowing to write correct code (especially C code) without borrow checker sure did spike with its introduction. Hence, my question. How do you know you haven't been writing unsafe code for years, when C unsafe guidelines have like 200 entries[1]. [1]https://www.dii.uchile.cl/~daespino/files/Iso_C_1999_definition.pdf https://www.dii.uchile.cl/~daespino/files/Iso_C_1999_definit... (Annex J.2 page 490)
- int_19h 2y ago
  It's not difficult to write a provably correct implementation of doubly linked list in C, but it is very painful to do in Rust because the borrow checker really hates this kind of mutually referential objects.
  - Ygg2 2y ago
    Hard part of writing actually provable code isn't the code. It's the proof. What are invariants of double linked list that guarantee safety? Writing provable anything is hard because it forces you to think carefully about that. You can no longer reason by going into flow mode, letting fast and incorrect part of the brain take over.

edflsafoiewq 2y ago

One example is a function call that doesn't compile, but will if you inline the function body. Compilation is prevented only by the insufficient expressiveness of the function signature.

lelanthran 2y ago

Rust prevents classes of bugs by preventing specific patterns. This means it rejects, by definition alone, bug-free code because that bug free code uses a pattern that is not acceptable. IOW, while Rust rejects code with bugs, it also rejects code without bugs. It's part of the deal when choosing Rust, and people who choose Rust know this upfront and are okay with it.

bigstrat2003 2y ago
> This means it rejects, by definition alone, bug-free code because that bug free code uses a pattern that is not acceptable. That is not true by definition alone. It is only true if you add the corollary that the patterns which rustc prevents are sometimes bug-free code.
- lelanthran 2y ago
  > That is not true by definition alone. It is only true if you add the corollary that the patterns which rustc prevents are sometimes bug-free code. That corollary is only required in the cases that a pattern is unable to produce bug-free code. In practice, there isn't a pattern that reliably, 100% of the time and deterministically produces a bug.