The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Arnaud,

 

thanks a lot for the detailed explanation – the “Register” process doesn’t seem to be documented in the reference manual, so this is very welcome.

 

I would say the trust base increase is not that much of a problem, as long as this can be switched off easily. I don’t see how this would be done in the current implementation of Int32 (other than copying the library and removing the register keyword). I would use such features mostly for interactive development and use the plain Coq implementation in overnight check runs, where speed doesn’t matter that much.

 

Btw.: has it been tried to use e.g. hex digit representations in Coq? This thesis analyses the speed up of multi-bit digit arithmetic in HOL:

 

FORMAL COMPUTATIONS AND METHODS by Alexey Solovyev, Pittsburgh, 2007

 

http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_(v._1.02).pdf

 

For 5 decimal digit numbers the speed up is about 2.5, from 10 decimal digits on one gets a speed increase of about 4 times for 4 bit digits.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928