[New Blog Post] Verifying Nand2Tetris Assembly Programs with Constrained Horn Clauses philipzucker.com/nand2tetris-ch #z3 #python #smt #verification
Conversation
There is a genuine internal debate here. Do I rewrite this in ocaml, probably a better choice for the job, or stick to a language that people tend to actually know? Pedagogically, I feel it makes a big difference.
2
Replying to
I probably would have preferred OCaml – I don't write it, but I do find it easier to understand and port than Python for this kind of thing, but I'm probably a weird outlier here.
If possible, having a tabbed option for Python/OCaml for the examples would be great. Perhaps saying at the beginning that you prefer OCaml and encourage people to learn it, but default to Python for wider reach. I understand that's more work though!
1
1
That’s a great idea! I suspect way beyond the level of polish I usually operate at