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
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
Replying to
Yeah, I saw that today! Yeah, I’m thinking it’d probably just be like ND, just with a different concrete syntax.
Replying to
Still worthwhile to think about these things. Looking at the same ideas through a different notation can be very fruitful.
1
1
Yeah, also wondering about how we could make our work more accessible. So that we could communicate to say, UX designers.
My other problem with the ND concrete syntax is that it is hard to understand the data flow directions. Requires copying the rules out or implementing a type checker first. Perhaps thats more a problem for syntax directed rules though...