4 ms·
This post shows 3 ways of doing it, including essentially the same way you'd do it in C. And it's exactly as dangerous as doing it in C is, but at least you ca
by empath-nirvana 3y ago
This post shows 3 ways of doing it, including essentially the same way you'd do it in C. And it's exactly as dangerous as doing it in C is, but at least you can isolate that dangerous code to one part of your code base.
- alexchamberlain 3y ago> you can isolate that dangerous code to one part of your code base. This is the whole point for me. There are loads of reasons fundamental data structures want to use behaviour the compile can't prove is sound, but humans can burn time discussing, proving the algorithms and testing the implementation. Then, you ask the compiler to prove all the simple glue stuff on top.
- hinkley 3y agoI suspect there's a type theory here where many cases of parent links essentially represent the exact same problem, and if you solve one, you can restate most/all of the others in this form and then it's proven too. You know that popcount bit counting device that treats a word of memory as a short SIMD instruction using the 32 or 64 bit ALU? I learned recently that compilers can detect that and emit popcount instructions if those are faster on the target architecture. I suspect if you can detect that, you could detect a safe parental reference device and let it pass the checker.