Random half-thought: I wonder if something like argument maps would be a less intimidating notation for defining programming language semantics than natural deduction: en.wikipedia.org/wiki/Argument_
Conversation
I'm imagining that you would define a series of 'nodes' for your argument map. With terminal nodes for your axioms. These would be your inference rules. The inputs and outputs of your nodes would follow the syntax of your language. You'd then wire them together to form proofs.
3