3 ms·
Writing correct code did not start after the introduction of the rust programming language
by yohannesk 1y ago
Writing correct code did not start after the introduction of the rust programming language
- Ygg2 1y agoNope, 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 1y agoIt'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 1y agoHard 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.