This comment is completely off the main topic, however, you are the first person I have encountered reading HN that is looking for a macro-assembler and theorem prover combo. I built a language to use just for my day to day and keep tinkering with it when I feel like it. One of the modes of operation is at least on the path to what you asked for. Right now, it is more of a generating C or C++ with full spectrum dependent types (i.e. it misses the convenience of the standard theorem provers). I find that it is quite practical for what I use it for, which is usually not at the full dependent type level, but it certainly works for me. I have toyed with making what would effectively be an assembly back end, but compiling to C++ usually fits my requirements. No real point in this comment, just wanted to cheer for another dev who seems to find interest in similar subjects.