I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. It isn't that the drawing doesn't exist. It is that you still have some freedom in how long certain parts could be. Crucially, not all. It could be that parts of the drawing are indeed fully specified.
Same can go with programs. You can constrain parts of it enough that you can answer some pretty specific questions. And similar to how a drawing with fewer lines is easier to constrain, a program that has restricted constructs can be easier to constrain.
>I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD.
That is just solution theory of a non-linear system of equations. The solution space can have exactly one solution (fully constrained), more than one (under constrained) or zero (over constrained).
To be honest I do not really see a connection.
I meant more as how to mentally model it in a way that can get someone across the line. My assertion is that caring about undecidability is almost certainly a waste of time for most people. That said, the reason we work in small chunks is often so that we can more easily answer questions about programs.
Moving the graphical drawing and constraints over to a symbolic system also helps see how many symbols it can take to cover a simple system.
Of course, the real reason for me thinking on this is that I'm playing with FreeCAD for the first time in a long time. :D