William, I understand the issue of proving "down to the metal".
Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK libraries in Common Lisp. Those libraries have a lot of coding tricks to avoid overflow/underflow/significance loss/etc. http://axiom-developer.org/axiom-website/bookvol10.5.pdf Two years ago I got Gustafson's "End of Error" book. His new floating point format promises to eliminate these kinds of errors. Unfortunately no current processor implements his instructions. So I bought an Altera Cyclone Field Programmable Gate Array (FPGA) in order to implement the hardware instructions. This is my setup at home: http://daly.axiom-developer.org/FPGA1.jpg http://daly.axiom-developer.org/FPGA2.jpg http://daly.axiom-developer.org/FPGA3.jpg http://daly.axiom-developre.org/FPGA4.jpg This is not yet published work. The game is to implement the instructions at the hardware gate level using Mealy/Moore state machines. Since this is a clocked logic design the state machines can be modelled as Turing machines. This allows Gustafson's arithmetic to be a real hardware processor. It turns out that shortly after I bought the FPGA from Altera (2 years ago) Intel bought Altera. They have recently released a new chip that combines the CPU and FPGA https://www.intel.com/content/www/us/en/fpga/devices.html Unfortunately the new chip is only available to data centers in server machines and I can't buy one (nor can I afford it). But this would allow Gustafson arithmetic at the hardware level. My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor has a verified hypervisor running on the ARM core http://www.provenrun.com/products/provenvisor/nxp/ So I've looked at the issue all the way down to the gate-level hardware which is boolean logic and Turing machine level proofs. It all eventually comes down to trust but I'm not sure what else I can do to ensure that the proofs are trustworthy. If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost. Tim On Wed, Apr 4, 2018 at 6:03 PM, William Sit <w...@ccny.cuny.edu> wrote: > ... > > [Message clipped]
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
