I should note that the lastest board I've just unboxed
(a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).
What makes it interesting is that it contains 2 hard
core processors and an FPGA, connected by 9 paths
for communication. The processors can be run
independently so there is the possibility
I'm familiar with most of the traditional approaches
like Theorema. The bibliography contains most of the
more interesting sources. [0]
There is a difference between traditional approaches to
connecting computer algebra and proofs and my approach.
Proving an algorithm, like the GCD, in Axiom is
