5 ms·

Hi Tim, >There is no point in publishing the work as open source since it is still in the active research phase. That sounds very interesting to me at least,

• daly 3y ago
  Having experience with prior open source work I'm not likely to release the current effort until I'm much closer to completion. The whole idea of CAS and Proof has already generated a hostile reception from both areas in my email stream. I've already proven that if I did release Axiom again I'm too socially inept to manage the process anyway. I'd release a technical paper or two but I'm no longer associated with CMU so I'm pretty much a "hobby researcher" I guess. The last Axiom presentation was the invited talk at Notre Dame prior to Covid. There are a lot of interesting things "in the works" though. One is the idea of "proof down to the metal" (aka Proof Carrying Code[0]). The use of (FPGA) field programmable gate arrays[1] and the RISC-V[2] architecture soft-implemented in the FPGA means that I can run the LEAN proof in parallel with the algorithm at the hardware level. This not only proves the algorithm correct, it proves the implementation correct. I have a few FPGAs. It's all fun and games but I have to wait to release it. [0] https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code [1] https://en.wikipedia.org/wiki/Field-programmable_gate_array https://en.wikipedia.org/wiki/Field-programmable_gate_array [2] https://en.wikipedia.org/wiki/RISC-V https://en.wikipedia.org/wiki/RISC-V