*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions*From*: Makarius <makarius at sketis.net>*Date*: Fri, 5 Jul 2013 13:39:02 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51D4A7E7.1000109@in.tum.de>*References*: <51D3205A.5030303@gmail.com> <51D46E5F.7000804@informatik.tu-muenchen.de> <51D49B99.20408@gmail.com> <51D4A7E7.1000109@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 4 Jul 2013, Manuel Eberl wrote:

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.

Makarius

**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

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

- Previous by Date: [isabelle] Tutorial 'Mechanised Reasoning in Economics' (Koblenz, Germany, 17 Sept.): early registration until 15 July
- Next by Date: Re: [isabelle] prove simple inequality
- 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