a fun thing to do is use haskell as a macro assembler with RecursiveDo for forward labels. simple attempt at encoding a dataflow instruction set
Conversation
Reminds me of “Coq: The world’s best macro assembler?”:
1
4
has been doing similar work in Lean:
Quote Tweet
Not possible to fit it all in one screen now, but my VCG now supports subroutines! Proof on right, code on left. It doesn't explicitly model the stack yet, though. Also supports jumping to a subroutine as a tail call rather than using jsr.
Show this thread
yes, i'm a big fan of that paper. my TODO list includes rewriting this assembler (and several other things) in Lean4 as an exercise, but admittedly my use case right now has nothing to do with proving anything. i just needed to write programs for my weird architecture!