Hacker News new | ask | show | jobs
by Ygg2 420 days 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.
3 comments
edflsafoiewq 420 days 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.
link
yohannesk 420 days ago
Writing correct code did not start after the introduction of the rust programming language
link
Ygg2 420 days 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_definit... (Annex J.2 page 490)

link
int_19h 419 days 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.
link
Ygg2 419 days 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.

link
lelanthran 419 days 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.

link
bigstrat2003 419 days 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.

link
lelanthran 419 days 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.

link