On Monday, 25 January 2021 at 21:40:01 UTC, Bruce Carneal wrote: > If I'm wrong, if it really is as you say "no problem", then the > RYU author sure wasted a lot of time on the proof in his PLDI > 2018 paper. Why is that? If the proof is for the algorithm then it has nothing to do with proving your implementation to be correct.