5 ms·

I wonder, can I define floating point arithmetic w/ this language?

• gmfawcett 7y ago
  Yes: https://hal.inria.fr/inria-00534854v1/document https://hal.inria.fr/inria-00534854v1/document https://xavierleroy.org/publi/floating-point-compcert.pdf https://xavierleroy.org/publi/floating-point-compcert.pdf
• cjfd 7y ago
  Of course. You can define more or less anything in this language. And, actually, someone has already done exactly that. See http://flocq.gforge.inria.fr/ http://flocq.gforge.inria.fr/ . Never used it myself so I do not know whether it is any good.
• philzook 7y ago
  As others have mentioned, it's possible and has been done in the FlocQ library. I don't have personal experience using them. I would expect proving properties to be somewhat challenging. There is a book available https://www.elsevier.com/books/computer-arithmetic-and-formal-proofs/boldo/978-1-78548-112-3 https://www.elsevier.com/books/computer-arithmetic-and-forma... You may also want to look at this thesis https://www.lri.fr/~melquion/doc/19-hdr.pdf https://www.lri.fr/~melquion/doc/19-hdr.pdf
  • philzook 7y ago
    As a side note, I believe native floating point operations are in the works. This is more of a speed benefit though? http://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIcs-ITP-2019-7.pdf http://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIc...