I propose doing anything super hard and rare outside the general model. Make the doubly-linked list in whatever tool supports easy verification. Things like Why3 and solvers for separation logic. Run that object code through lots of testing with runtime checks for the specified behavior. If it passes, it's probably earned the right to be wrapped for use in the memory-safe code.
This use case is also why I prefer more research funding to go to verified solvers than to manually-verified algorithms. They'll get more real-world use on hard problems. Well, that and test generators. They complement each other. The testing tools are more cost-effective, too.
https://rust-unofficial.github.io/too-many-lists/
I propose doing anything super hard and rare outside the general model. Make the doubly-linked list in whatever tool supports easy verification. Things like Why3 and solvers for separation logic. Run that object code through lots of testing with runtime checks for the specified behavior. If it passes, it's probably earned the right to be wrapped for use in the memory-safe code.
This use case is also why I prefer more research funding to go to verified solvers than to manually-verified algorithms. They'll get more real-world use on hard problems. Well, that and test generators. They complement each other. The testing tools are more cost-effective, too.