alt Hacker News> It can also be quite possible to invent structures which are valid but have no valid path to creating them.
I'm curious if you have an example of such a structure?
Pedantically: if, for every valid tree, there exists a bidirectional path to the empty root node, there's always at least one path between all given pairs of valid trees ... albeit one that no developer would ever take.
You are quite right to call this out - and quite right in general. With AST verification alone your statement holds strongly.
I was remembering a professor I had who was very into formal verification and had an IDE that would only accept valid programs - however his validity checks were more than just tree based, they involved passing a type check. Which now you've called me on it, is quite definitely beyond valid AST editing.
The base case: if you have a structure with a mandated cyclical reference that doesn't accept a second (e.g. nil) type, you cannot construct it without creating an intermediate invalid program. This doesn't tend to show up if the cyclical reference is all the same type (A1 -> A2 -> A1) because you can often cheat and self reference, but it does if it is different types (A1 -> B1 -> A1). You can't construct an A without a B, which cannot be constructed without an A.
But that's still not a problem you cry! And quite right, you can edit the type itself to remove and re-add the reference.
That is until the type is built into the language, or a library.