this looks really cool!<p>I think it&#x27;s weird that the author dings matlab and mathematica for being unable to do counterfactual reasoning. matlab and mathematica are computational tools, they don&#x27;t do &quot;reasoning&quot; the way that say coq or other proof assistants do. and proof assistants can do counterfactual reasoning, so what&#x27;s the deal? beyond that it would take a lot of work to encode these graphical diagrams into coq I guess...