3 ms·
People wanting to go from math to machine might like a work that starts with formal specs. http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf http://www.cl.c
by nickpsecurity 10y ago
People wanting to go from math to machine might like a work that starts with formal specs.
http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf
The resulting ML can be compiled to assembly by verified, CakeML compiler.
https://cakeml.org https://cakeml.org
- iheartmemcache 10y agoIt's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;) [1] https://www.cse.unsw.edu.au/~cs4161/lect.html https://www.cse.unsw.edu.au/~cs4161/lect.html
- nickpsecurity 10y agoGlad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically verified in PVS as part of Verisoft project. They did OS and C subset for it. Adding it to L3 and Myreen et al's toolkit for doing machine code in Isabelle/HOL would let their spec-to-machine-code verifications run on a verified processor. Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.
- pjmlp 10y agoThanks as well, I join my opinion to iheartmemcache's one. :)