I'm not sure I understand all of what they're doing there, but I did read the referenced Doligez-Leroy-Gonthier paper a while back and I am glad someone is doing something with that in a non-academic (maybe?) context. That paper looked promising to me when I read it, but I basically had no faith that it would ever make it out of academia because the algorithm is so complex. It took me a really long time to think I understood it, and it's one of those things I actually am not confident I could implement even when I understood it (I certainly don't understand it now).
replies(1):