Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Improving the world for 2014, one programmer at a time

I move that all computing devices be equipped with a small explosive charge, set to explode when someone refers someone else to Goldberg's What Every Computer Scientist Should Know About Floating-Point Arithmetic without the referrer emself having read it.

It would not have to be lethal. I could be content if the apparatus maimed the user into harmlessness.

For what it is worth, the advice I wish I had received instead of being suggested Goldberg's essay the first time is:

  1. Print numbers in hexadecimal format as often as you can (%a in C99). Input them that way when it makes sense.
  2. Don't worry, floating-point numbers are just bits. Stop listening to anyone who tries to confuse you with generic reasoning about an arbitrary base β.



1. On Thursday, December 26 2013, 22:01 by yannick

For what it's worth, I just read the incriminated paper, after being referred to it several times by a more knowledgeable colleague (who knows perfectly well what the paper says, contrary to your referrers), and found it quite interesting. I had rather blurry ideas on subnormal numbers and representation of special numbers, that the reading cleared up! I liked in particular the section on Langues and Compilers, which applies as well to those writing analyzers like me. It contains a nice equality that cannot be trusted to hold for floating-points: 0 - x is not the same as -x (due to positive and negative zero). One more to add to the nice listing that Xavier Leroy presented during a talk at POPL 2011 (see slide 44 of, that I had glued to my monitor for years. But I'd be interested to know if you have better readings regarding floating-point arithmetic oddities.

2. On Wednesday, January 8 2014, 17:29 by pascal
Hello, and happy new year.
> But I'd be interested to know if you have better readings regarding floating-point arithmetic oddities. 
A must-read article is David Monniaux's:
This article is fortunately slowly becoming dated: the SSE2 instruction set implements IEEE 754 single- and double-precision, and started being available on desktop processors in 2002. PowerPC provides double-precision exactly, and so does ARM. A modern GCC should be made to generate SSE2 instructions, and if that isn't an option for some reason, can compile C code according to the deterministic semantics laid out by Joseph S. Myers:
This post that was published only a few months after David's article, although it will take several more years to take full effect in practice (several of the GCCs available to me predate Joseph's patch), and the psychological consequences may last forever, as the tales of unpredictable floating-point are handed down from programmer to programmer, the way primitive superstitions were.