Further to the previous post. The talk on Hazel is fascinating.
I’ve been thinking for a while about the importance of being able to program “in your own order” ie. fill the blanks of your decision making about your program as and when you have that information available to you / or as you feel like tackling that problem. And leaving the undecideds and unknowns until later.
Holes in Hazel and other theorem provers offer that capacity in the small. And obviously tied to some advanced type theory which is a bit beyond me, but I think I grok the basic ideas. And, yes, having a formalization of the unknowns is a powerful idea.