
<!DOCTYPE html>

<html>

  <head>

    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">

  </head>

  <body>

    <p>I remember having seen a talk about that ... but I cannot find

      any matching papers :(</p>

    <p><br>

    </p>

    <div class="moz-cite-prefix">On 20/11/2025 15:40, Lawrence Paulson

      wrote:<br>

    </div>

    <blockquote type="cite"

      cite="mid:b8105aaa-640c-4c21-bc60-c486f9db1d91@Spark">

      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">

      <title></title>

      <div name="messageBodySection">

        <div dir="auto">I know that converting a floating point number

          to decimal notation is tricky, but we must've had correct

          algorithms for decades now. I wonder whether anybody has

          formalised one :-)</div>

      </div>

      <div name="messageSignatureSection"><br>

        <div class="matchFont">Larry</div>

      </div>

      <div name="messageReplySection">On 20 Nov 2025 at 13:21 +0000,

        Achim D. Brucker <a class="moz-txt-link-rfc2396E" href="mailto:adbrucker@0x5f.org"><adbrucker@0x5f.org></a>, wrote:<br>

        <blockquote type="cite"

style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">

          <br>

          <div>This is also my assumption.  The values used by me in the

            below example<br>

            are after pretty printing (i.e., convertio to strings).<br>

            <br>

            The actually value stored is

            0.070820772089064121246337890625 (decoding<br>

            it "manually", following the standard). Trying to print it

            in a small C<br>

            programm gives 0.00708207720890641212, which seems to be the

            offical<br>

            decimal represenation according to the standard. IEEE754  is

            not easy ...<br>

          </div>

        </blockquote>

      </div>

    </blockquote>

  </body>

</html>