The need for a glossary came up on Discord today.
This needs some more work, but I think this is a good start. I'm still
happy to update it if anyone has suggestions, of course. I haven't
started sprinkling pointers to the glossary from other places, so
users will only discover it by browsing the `docs/` directory.