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.

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:
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

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

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.


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <w...@ccny.cuny.edu> wrote:

> ...
> [Message clipped]
Axiom-developer mailing list

Reply via email to