Poster here. I re-read this paper about once a year. I continue to think that it may be one of the most important papers I've read. As someone who works on high-reliability safety-critical real-time systems (automotive, avionics), being able to work in an environment where I could prove semantic properties of assembly code is pretty close to my dream -- the cost of demonstrating code correct is already so much higher than the cost of writing the code that the incremental cost of going to assembly seems minor, if there's even a small payback in time to demonstrate correctness. In practice, I think my dream language would be a relatively rich macro assembler plus a (guided, greedy) register allocator, designed entirely to simplify and allow semantic proofs. I don't really have a sense as to whether Coq (Rocq) is the right answer today, vs other options; or if there's a newer literature advancing this approach; but I'd truly love to see a deeper focus of making low level languages more useful in this space, rather than moving towards more constrained, higher level languages.
This paper reminds me of a class assignment in grad school where the prof asked the students to write a compiler in Coq for some toy Turning-complete language in a week. Having no background in compiler design or functional programming, I found it daunting at first, but eventually managed it. The Coq language's rigor really helps with something like this.
I wonder if AI's compute graph would benefit from a language-level rigor as of Coq.
It's a bit of an awkward syntax to get a reliable assembler. Does it at least allow you to prove the behaviour of a larger block of assembly? For example, could I use it to prove that a block of assembly is equivalent to a given set of operations?
Can you give an example? With something like Figure 1 of the paper converted to a convenient form for Lisp (s-expressions, presumedly), and assuming a function to convert it to binary, what would it look like to prove correctness of that assembly in Lisp? What's the ecosystem of proof assistants that would get you there?
You can write a prover like Coq in a Lisp, but, though it's easier than doing it in C, I think it's somewhat harder than doing it in something like OCaml. ACL2 is an example of such a thing.
This is great. I honestly never thought of computer as a register state and instructions/asm commands as functions applied to it. But that makes so much sense.
A particular emphasis of our work on machine code verification is on using Coq as a place to do everything: modelling the machine, writing programs, assembling or compiling programs, and proving properties of programs.
Coq’s powerful notation feature makes it possible to write assembly programs, and higher-level language programs, inside Coq itself with no need for external tools."
Looks very promising! There is definitely something here!
13 comments
[ 2.6 ms ] story [ 33.0 ms ] threadI wonder if AI's compute graph would benefit from a language-level rigor as of Coq.
Coq: The world’s best macro assembler? (2013) [pdf] - https://news.ycombinator.com/item?id=8752385 - Dec 2014 (61 comments)
A particular emphasis of our work on machine code verification is on using Coq as a place to do everything: modelling the machine, writing programs, assembling or compiling programs, and proving properties of programs.
Coq’s powerful notation feature makes it possible to write assembly programs, and higher-level language programs, inside Coq itself with no need for external tools."
Looks very promising! There is definitely something here!