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
Replying to
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
Surely this is not a new idea? 🤔