[plt-dev] Re: [PRL] Programming Languages in the Code of Federal Regulations

Thanks, I know. 





On Apr 26, 2010, at 10:28 PM, Pete Manolios wrote:

> Exact rational arithmetic is clean and convenient to reason about
> (that's what ACL2 uses), but a major problem is that one often really
> wants the reals. For example, are you sure you won't need operations
> such as square root? pi? e? log? sin? ...
> 
> Another problem is that if a lot of computation is involved, then
> exact rational arithmetic can easily get really slow.
> 
> If you decide you want the reals, chances are you'll decide to give up
> on exactness. One option to consider then, is to explicitly specify
> the error bounds you are willing to tolerate. Then you can use
> techniques such as interval arithmetic.
> 
> Pete
> 
> On Mon, Apr 26, 2010 at 9:02 PM, Matthias Felleisen
> <matthias at ccs.neu.edu> wrote:
>> 
>> I thought it was obvious that I had an exact rational arithmetic in mind, with ways to translate them into printable amounts. Furthermore, in case you're wondering, I would also specify the FFI to force the foreign language to use the same operations as the DSL and to not provide any conversions to and from this data type to a 'foreign' datatype. -- Matthias
>> 
>> 
>> 
>> On Apr 26, 2010, at 7:36 PM, Pete Manolios wrote:
>> 
>>> Following the IEEE 754 floating-point spec is not easy. For example,
>>> see "The pitfalls of verifying floating-point computations" by David
>>> Monniaux. Even if floating point is handled in a reasonable way, it is
>>> still floating point, so many "obvious" properties, like associativity
>>> of addition, do not hold. That is, there is no way to satisfy
>>> Matthias' criterion number 2 if we use floating point (unless
>>> "intended mathematical meaning" below means IEEE floating point).
>>> 
>>> 2 Programs should have the intended mathematical meaning.
>>> 
>>> 
>>> 
>>> On Mon, Apr 26, 2010 at 6:19 PM, Paul Steckler <steck at stecksoft.com> wrote:
>>>> R6RS suggests, but doesn't require, that Scheme implementations follow
>>>> the IEEE 754 floating-point spec.
>>>> So you don't get behavior guarantees simply by choosing "Scheme" as
>>>> your language.
>>>> 
>>>> Years ago, Turbo Pascal had a binary-coded decimal (BCD) type that was
>>>> especially suited for doing
>>>> financial calculations, avoiding some of the representational problems
>>>> of IEEE 754.  Something like
>>>> that might figure in a DSL for the feds.
>>>> 
>>>> -- Paul
>>>> 
>>>> On Tue, Apr 27, 2010 at 12:31 AM, Matthias Felleisen
>>>> <matthias at ccs.neu.edu> wrote:
>>>>> 
>>>>> Following Jay's and Jordan's example I have submitted my own response. A
>>>>> scribbled version is available at:
>>>>> 
>>>>>  http://www.ccs.neu.edu/home/matthias/Thoughts/Python_for_Asset-Backed_Securities.html
>>>>> 
>>>>> Thanks for all the feedback -- Matthias
>>>>> 
>>>>> 
>>>> 
>>>> _______________________________________________
>>>> PRL mailing list
>>>> PRL at lists.ccs.neu.edu
>>>> https://lists.ccs.neu.edu/bin/listinfo/prl
>>>> 
>>> 
>>> 
>>> 
>>> --
>>> Pete Manolios
>>> Northeastern University
>>> http://www.ccs.neu.edu/home/pete
>> 
>> 
> 
> 
> 
> -- 
> Pete Manolios
> Northeastern University
> http://www.ccs.neu.edu/home/pete