An article you might find helpful is this one on why imperative algorithms are harder to mathematically verify than functional ones: https://semantic-domain.bl

An article you might find helpful is this one on why imperative algorithms are harder to mathematically verify than functional ones: https://semantic-domain.blogspot.com/2018/04/are-functional-programs-easier-to.html https://semantic-domain.blogspot.com/2018/04/are-functional-... You don't need to be a mathematician to follow it with this excerpt summarizing its key point: "The difficulty of imperative programming arises from the combination of state, aliasing and procedure calls. Any two of these features can be handled without that much difficulty, but the combination of all three effectively makes reasoning (nearly) as difficult as correct concurrent programming. " The garbage-collected languages let you ignore the aliasing problems with a performance penalty. Rust in safe mode without GC forces you to (a) deal with it and (b) deal with it in a way that works for all inputs (type/memory safety). That usually requires mathematical verification using tools such as separation logic. Rust's method is much easier to use with tradeoff of limitations on expressing code in certain ways. Folks that get along with the borrow-checker say it helps to design the program around data and easy methods of using it versus starting with control flow forcing it on a data structure. I'll also add that linked lists are inherently hard to get right on all inputs regardless of low-level language. They're actually a popular way to test new, mathematical methods for specifying and proving algorithms correct. Fortunately, Rust folks have a goto write-up on linked lists in their language: https://cglab.ca/~abeinges/blah/too-many-lists/book/ https://cglab.ca/~abeinges/blah/too-many-lists/book/