All, This paper about ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS https://alastairreid.github.io/papers/popl19-isasemantics.pdf is interesting. It seems to provide a "base case" for proving programs correct. In particular, they seem to be able to generate proof code for various provers, including Coq.
One of the criticisms about "proven programs" is that they tend to ignore implementation details. But given a lisp variant, Milaw, that is proven to the hardware instructions this new step is really important. A proof of the machine instructions, a proof of milawa on top of those instructions, a proof of lisp extensions on top of milawa, and a proof of Axiom's spad language on top of lisp turns into a fully validated tower. It appears that all of this (and it is an impressive pile) can be developed in Coq. Also of interest, while I was part of the CMU CERT effort I developed the ISA for the Intel 32 bit processor [0]. My program reads Intel binary and generates "Conditional-Concurrent Assignment" semantics. I may be able to re-target the back end to their Sail language which would provide ISA semantics for Intel 32 in Coq. Tim [0] Daly, Timothy Intel Instruction Semantics Generator <http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/intel/intel.pdf> SEI/CERT Research Report, March 2012
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer