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.
Replying to
There aren’t usually any “objections” in a programming language. Without that, isn’t this essentially natural deduction notation?
You might also be interested in kialo.com for an interactive interface to something like this for structuring online arguments.
1
Yeah, I saw that today! Yeah, I’m thinking it’d probably just be like ND, just with a different concrete syntax.
2
Show replies
Could be! 🧐
1
Show replies