Coq: The world’s best macro assembler? (2013)

For a long time I thought I wanted a macro assembler + theorem prover instead of Rust and now I know there is such a thing.