Re: [isabelle] Isabelle Foundation & Certification



Makarius:

>OCaml is much less safe than SML, e.g. strings are
>mutable, ints overflow at unspecified word size without
>any exception,

I think the newest OCaml support immutable strings?
And if in the kernel you would use nums instead of ints,
then the second problems would be gone too?  (It would be
interesting to know how much of a hassle this last change
would be.  And maybe you only would need to go through
nums when you actually calculate with ints in the kernel?
Does this even happen, and if so, in which functions?)

Freek




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.