Because Nock is so simple (just a few substitution rules) I wonder if it'd be reasonable to formalize it in a theorem prover like Coq, or Agda to ensure correctness.