Well-formedness dev guide page

[fallible-algebra]

Initial work off of discussions with boxy + chasing hyperlinks. Part of #2663.

Few unsolved items here:

• Conceptual: Items "contain" Terms? Is this the right way to say this? I imagine so, syntactically, but I need a vibe check.
• Remove the "boxy said so" citations
• "Term"¹ needs to be better specified as a concept. Maybe added to the glossary.
  • May end up as "Type-Level Term" again.
• Wfck doesn't appear on its own, but as item-wfck or term-wfck (alt: term well-formedness checking for ths one specifically).
• Run the formatter that deals with maximum line length.
• Remove unused links

I've also ended up doing some syntax here "from scratch", which I could use some input on. Specifically for showing off obligations I've done:

<Items or Terms>
---
<Obligations and (relevant) Substitutions>

If this works fine, cool. Otherwise, open to being told to do it a different way :)

Finally, I'm putting this in an analysis subfolder as I've been told we need to do some structural reordering of the mdbook directory, and this should eventually live in an analysis subfolder so might as well have it there now.

Footnotes

1. This was "Type-Level Term" in these files before I find-replaced it all to Term, which is maybe too vague to our target audience. ↩

[BoxyUwU]

another round of feedback, I think slightly more nitpicky than last time? though still mostly just based around the general structure rather than too much about individual sentences/paragraphs/whatever

View changes since this review

[BoxyUwU]

hell yeah :) this feels about right structurally to me

View changes since this review

[BoxyUwU]

diff of the headers lol

+- Well-Formedness
-- Well-Formedness of Items and Type-Level Terms
+   - What is Well-Formedness
+     - talk about the abstract concept. wfness isnt a specific thing its just the nebulous concept of things being 'correct'. we generally use it informally all over the place just to talk about us having checked something in the type system.
+     - there are some actual places in the compiler that use the wf terminology specifically. item wfck and well formed obligations
   - Well-Formedness of Type-Level Terms
    - Obligations for Well-Formedness
    - When Type-Level Terms Are Well-Formed
    - We Don’t Need Normalization (Yet)
    - Const Generic Arguments
 -  Well-Formedness of Items
    - We (Sometimes) Need Normalization
    - Global and Trivial Bounds
 - When We Don’t Fully Do Well-Formedness Checking
    - Trait Objects
    - Free Type Aliases
 - “Well-Formed” or “Wellformed”?
 - What Well-Formedness Isn’t

vague thoughts about adding a new header at the top. briefly talked about this to u on zulip but not much. I think that the right framing is probably to start by going "hey wfness is a nebulous informal concept" and then go "there are a couple concrete places in the compiler that are named after this nebulous informal concept".

[BoxyUwU]

its somewhat arbitrary but im not a huge fan of saying stuff like "perform term well-formedness checking" and would rather we say things like "check terms are well-formed". im not sure I can justify why this is the case but it feels quite off to be saying the former instead of the latter 😅

i think this is the nitpickiest of all my reviews but i think we're pretty much There with this doc at this point?

View changes since this review

[BoxyUwU]

get nitzoned lmao

View changes since this review

[tshepang]

are the intermediate commits worth keeping... should we squash

[fallible-algebra]

I'm comfortable with a squash here