[ef4]

Agreed, but that's not what they did here. They didn't prove the program is correct, they proved the algorithm is correct. It remains to be seen how closely the program actually implements the algorithm in the paper.