Please write a short paragraph as a comment in the class forum thread about any one of the following discussion questions (you need to respond to just one question of your choice to get credit, though you're free to write more if interested):
- Do you think that proofs by reflection are a valuable approach to proofs regardless of the underlying foundations? Or are there proof assistants with foundations for which proofs by reflection may not be useful? Why or why not?
- What tradeoffs do you perceive between proofs by reflection and other styles of proof? Which do style you find most intuitive, and why? When might you choose one you find less intuitive over one you find more intuitive?
- If you were designing a proof assistant from scratch, would you include any special support for proof by reflection? What kind of support might you add to make proof by reflection easier?
- Is there anything about the examples Adam goes through that you find confusing? What and why?
- Find an answer from someone else who pointed out something confusing for the question above. If tasked with doing so, is there any way you might build interfaces, tutorials, documentation, or automation to make that thing less confusing?
- Write a paragraph responding to someone else's comment in the discussion forum.
- Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.
You may want to look at other people's responses before class in order to shape the discussion. And again remember that you need to answer just one question to get credit, though you are free to answer more if interested.