logoalt Hacker News

Normal_gaussiantoday at 1:01 AM0 repliesview on HN

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.