*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 04 Jul 2013 00:38:31 +0200*In-reply-to*: <51D49B99.20408@gmail.com>*References*: <51D3205A.5030303@gmail.com> <51D46E5F.7000804@informatik.tu-muenchen.de> <51D49B99.20408@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

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. Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Christoph LANGE

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

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

**References**:**[isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Christoph LANGE

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

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

- Previous by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Previous by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list