Discussed at the time:

Coq: The world’s best macro assembler? (2013) [pdf] - https://news.ycombinator.com/item?id=8752385 - Dec 2014 (61 comments)