On 02/11/2016 15:58, Lawrence Paulson wrote:
I have to say, I’m absolutely mystified by the response to my suggestion.

This is a nontrivial change in the semantics. The programming language community has tried to get away from the "looks ok" approach to "here is some sound reasoning why it is ok". I could indeed not construct an example where a new incorrect result arises because of a caught over/underflow exception (only new ways to construct results that could already arise before). But that isn't exactly a proof (although the proposition may well be a thm).

Otherwise I agree with Makarius.


MetiTarski, which during execution relies heavily on large integers,
nevertheless benefits to the tune of 30% to having all other integers
fixed-precision. During its execution, Isabelle makes very heavy use of small
integers, in the representation of bound variables and flexible variables, which
are renamed by having an offset before each and every resolution step.

We have spent a lot of time discussing problems caused by the cost of regression
testing, and now we have the possibility of reducing that by 30%.

As to changes in behaviour that could be caused by overflows, I checked:
exception Overflow is explicitly caught in only two places throughout the
sources, both in HOL decision procedures (and therefore well outside the kernel)
while the wildcard exception is caught in three places in Pure. No exception
handlers had to be added when I converted MetiTarski to use fixed integers. An
uncaught exception doesn’t prove anything, of course.


On 2 Nov 2016, at 14:43, Makarius <makar...@sketis.net
<mailto:makar...@sketis.net>> wrote:

On 02/11/16 15:30, Lawrence Paulson wrote:

I actually can’t think of many places where Isabelle would need large
integers, so it would probably benefit even more than MetiTarski does.

"Can't think of" merely indicates a lack of empirical tests, against the
Isabelle repository and AFP. Afterwards the situation usually looks
quite different, and the initial hypothesis needs to be changed.

When we moved to proper int by default some years ago, there were
several tool implementors approaching me, asking to be delivered from
the curse of many different "int" types.

We also have conceptual reasons to stay true to the concept of an
integer that is an integer, a string that is a string etc. -- and thus
not using a machine word instead of an integer, or a "char" type that
cannot hold a textual character (not even in Unicode). Isabelle/ML is
meant to be a programming environment free from bad jokes like that.

Nonetheless, I do think that proper use of machine words in isolated
situations can help, but they should not be called "int" and used by


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to