Internal & community feedback

[WhatisRT]

I'm collecting a bunch of feedback I've gotten yesterday here 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 Eliminate Boolean properties #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.

[WhatisRT]

From a conversation with Pi on discord:

• About the section on crypto primitives:
  
  The notion of KeyPair is confusing: why is it a triple? After cleaning up this confusion, I asked whether to hide it behind the curtain. This is his reply:

  Definitely hide it behind the curtain in the PDF, IMO; the source agda files are your source of truth if you want things out in the open, but the PDF should be focused on clarity and understanding, and things that aren't contributing to that just add to that "weariness factor" that comes from trying to read a document by this and hitting branches on the way down

• He then said this, which I think is completely fair as well:

  Also, sections 1.5, 1.6, and all of section 2 could use some work I think; Unless I'm missing something, they basically say "Set theory works the way you'd expect it to, but we had to define our own types for complicated Agda reasons", meaning they fall into that bucket of being more confusing than helpful:
  Either you spend time reading it scratching your head wondering what is actually different from the math you know and worrying that some subtle difference is eluding you
  or, you're not super familiar with topics like sets, maps, and relations in the first place (because you're a programmer, not a mathematician), and this doesn't serve as a good introduction to those topics

  So, if you're trying to make it approachable to someone without the neccesary background, it needs to walk them through things slower, or at least let them know that they'll have a much better time if they go teach themselves those topics first.

  If you're just providing preamble definitions for the agda reader, then it probably makes a lot more sense as an appendix than something you're asking someone to invest time in understanding (and making them doubt whether they do understand!) right out the gate.

  I think I wrote these sections for the Agda workshop in Italy 2 years ago, so they were for a different target audience. But I agree that outside of an audience that's very interested in Agda they make less sense.