Hacker News Reader

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

The resulting ML can be compiled to assembly by verified, CakeML compiler.

It'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

Glad 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.

Thanks as well, I join my opinion to iheartmemcache's one. :)

Reply on news.ycombinator.com