[Ygg2]

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)

[int_19h]

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]

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.