Sorry, I was probably unclear. I imagine Cutter just tells you what each opcode does, no? gcc.godbolt.org does that too, with links to the ISA docs. But here I

Sorry, I was probably unclear. I imagine Cutter just tells you what each opcode does, no? gcc.godbolt.org does that too, with links to the ISA docs. But here I mean that in the ChocoPy code you get explanations of what instructions do in the context of the program's semantics, i.e., how they relate to a higher-level view of what's going on. An example: .globl $print $print: # Function print lw a0, 0(sp) # Load arg beq a0, zero, print_6 # None is an illegal argument lw t0, 0(a0) # Get type tag of arg li t1, 1 # Load type tag of `int` beq t0, t1, print_7 # Go to print(int) li t1, 3 # Load type tag of `str` beq t0, t1, print_8 # Go to print(str) li t1, 2 # Load type tag of `bool` beq t0, t1, print_9 # Go to print(bool) print_6: # Invalid argument li a0, 1 # Exit code for: Invalid argument la a1, const_4 # Load error message as str addi a1, a1, @.__str__ # Load address of attribute __str__ j abort # Abort Note that the different occurrences of lw and li explain the meanings of the magic constants in the code. This would be pretty hard to do from disassembly alone.