On Mon, 7 May 2012, John Harrison wrote:
> | * Standard ML with its no-sense semantics
>
> This reminds me that last time I looked at SML (which was admittedly a
> long time ago) the formal semantics left integer arithmetic almost
> completely undefined, and at least one implementation used machine
> arithmetic. Has that situation now changed?
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.
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.
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.)
> Note that F# has immutable strings and is otherwise pretty close to core
> OCaml, and it seems to be getting quite popular. I'd use it more myself
> if it were a bit more Linux-friendly, and I have the idea of porting HOL
> Light to it there in the back of my mind somewhere. I think the code for
> my theorem proving book would be an easier first step, though.
F# and the underlying .NET runtime is certainly a quite different
category. Its main disadvantage is the obvious MS bias of .NET, but Mono
might be able to do it, although I did not meet any excited users of .NET
on Linux so far.
Makarius
------------------------------------------------------------------------------
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
