4 ms·
The way the exploit works isn't actually that bad. It just has to do with exploiting Coq's assumption that its bytecode VM evaluator is equivalent to normal CBV
by tel 12y ago
The way the exploit works isn't actually that bad. It just has to do with exploiting Coq's assumption that its bytecode VM evaluator is equivalent to normal CBV reduction. Turns out that's false---though that was certainly always a potential weakness in that assumption.
- jerf 12y agoYes, if I did not make it clear, what was actually demonstrated here was not the sort of scarybad mathematical weakness that can only be extracted from a long proof that I was talking about, it's basically just a bug in Coq, and in the long term has little consequence other than providing a bit of fun.