Internal & community feedback

I'm collecting a bunch of feedback I've gotten yesterday [here](https://discord.com/channels/981862537513545788/1334557903369142333) in this issue. I'd like to address as much of this as we can so that hopefully the spec becomes a more accessible piece of documentation.

- [ ] Some people dislike the natural deduction notation, this definitely needs an explanation. It may be extra helpful if we can give a simple example to show that it's not difficult to translate it into executable code (Python as a target language was suggested here).
- [ ] More generally, the context of the state machine formalism is unclear. Why is it a state machine? Why do we express the rules the way we do?
- [ ] Names are confusing sometimes. Why is the unique UTXO rule called `UTXO-inductive`? (Answer: historical reasons that go back to a Shelley-era design that didn't even make it into the final Shelley spec)
- [ ] There were a bunch of specific complaints about `feesOK`, most of which just happened to be fixed by #649. One thing that's missing is that the implication is pretty confusing here. `if_then_else ⊤` is equivalent to the implication here and might be less confusing.

Maybe we should also try to specifically invite feedback on our readme or in the PDF itself. The more feedback we get the less we have to rely on our own opinions as to what is and isn't confusing.