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, I'd appreciate being able to take a peek.
>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, I'd appreciate being able to take a peek.
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
[1] https://en.wikipedia.org/wiki/Field-programmable_gate_array