Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
2013-07-03 23:38 Manuel Eberl:
> 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.
> 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.
Thanks for pointing out. Indeed BigInt would be the right type to use
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
Submission until 12 July; http://www.iaoa.org/womo/2013.html
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
This archive was generated by a fusion of
Pipermail (Mailman edition) and