Hi Makarius,
| This must have been a really long time ago. I've got exposed to SML in
| 1993 and it had already the integer arithmetic defined properly, as far as
| I remember. In any case it is all hard and fast in SML'97. The Standard
| document is not perfect, but its flaws are tiny compared to anything else
| in the greater ML family, or the world out there.
I was thinking more specifically of the formal semantics in "The
Definition of Standard ML", which said almost nothing about integer
arithmetic. But for all I know that document may also have evolved.
| For SML type int you always get a correct approximation of true integer
| arithmetic, i.e. overflow is guaranteed to produce an Overflow exception.
| The size of integers is not specified, unless you use one of the definitive
| int sizes from the library, which I don't like very much. In Isabelle/ML we
| make sure that the user always gets the big integers that never overflow in
| practice, so the program is also total in that sense.
I still don't much like the fact that SML leaves integer arithmetic
underspecified. For those of us in symbolic computing, it would be
really nice if we could just treat integers as integers and the only
failure could be running out of memory. Still, I suppose the main goal
for us is partial correctness (if you get an alleged theorem, it's
valid), so in that sense giving an exception instead of quietly
wrapping is a significant improvement.
| Poly/ML manages to implement proper big ints efficiently, with
| silent upgrade of machine word arithmetic to library functions,
| when overflow occurs in the hardware. (This is actually a
| vulnerability in the sense that the GMP library used here is very
| complex and not verified, as far as I know.)
Does the Isabelle core actually depend on the correctness of integer
arithmetic? There are two uses of ints in the HOL Light core that I
can think of:
* The term ordering uses {-1,0,1} for {<,=,>}. It might be nice to
replace this with some custom ternary type, but at least this
doesn't get into the range where machine arithmetic is an issue
(except on a 1-bit machine, perhaps).
* Each type constructor has an int for its arity and when the user
tries to construct a type with it, this value is compared with the
length (also as an int) of the list of type arguments. So in
principle you could declare a type constructor with arity n and
later give it n + 2^31 arguments (on a 32-bit platform). This is
a bit of a rough edge, but of somewhat academic interest, and I
don't think it implies a soundness problem (you could imagine
allowing type constructors with the same name but different
arities). Still, maybe Mark Adams will find a flaw in that
reasoning and then I'll change to using unit list instead of int!
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
