Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions

On 07/03/2013 11:46 PM, Christoph LANGE wrote:
> I am nowhere near an _experienced_ Scala programmer yet, but
> sufficiently capable of writing wrapper functions that, e.g., convert
> set[Nat] to List[Int] […]

At the danger of being called a nitpicker: this sort of thing can cost
you the programme correctness that you have so painstakingly ensured
with Isabelle, since Int in Scala is subject to integer overflow. I have
heard stories of "verified" code producing horribly wrong results
because people did not take integer overflow into account. These stories
were from code verified with a verification condition generator and
automated theorem provers; the Isabelle-generated code is, of course,
not affected by things like this, but when writing wrappers around it
that use native integer types, the same caveats apply.

Personally, unless I do some heavy number-crunching, I use the
arbitrary-precision Integer type (in Haskell) just to be sure –
especially with Isabelle-generated code.


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