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
Replying to
Reminds me of “Coq: The world’s best macro assembler?”:
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
1
1