Also we cannot forget Henrik Imhof's work on partial fixed point logic which seems very relevant for TML. The logic is something I'm unfamiliar with so I don't discuss it in detail in this post but it is something critical for the self defining property of TML. This is something for Ohad to describe best in my opinion because logic is not standard knowledge common for programmers.

The fact that the code works represents a breakthrough because it's a practical implementation where "the proof is in the pudding" as they say.