I've been looking forward to these. Based on my experience, I'd guess that programs simple enough to be proved may not provide satisfactory performance, especially for large exponents. I'll have to take a look when I get the papers.