3 ms·
Great find and writeup. As an aside, this is the type of a problem that I think model checkers can't help with. You can write perfect and complicated TLA+/Lean
by wy1981 1y ago
Great find and writeup.
As an aside, this is the type of a problem that I think model checkers can't help with. You can write perfect and complicated TLA+/Lean/FizzBee models and even if somehow these models can generate code for you from your correct models you can still run into bugs like these due to platform/compiler/language issues. But, thankfully, such bugs are rare.
- jraph 1y agoYep. Model checking is for checking that your design is sound, basically, not at all the implementation. For the implementation, you can use certified compilers like CompCert [1], but: - you still have to show your code is correct - there are still parts of CompCert that are not certified [1] https://compcert.org/ https://compcert.org/