>>12659262how difficult can it be to implement this in Python or JavaScript
you need: Languages Proof Logic (1999) and Shorter Model Theory (1997) or equivalent
you can get both of those at genDOTlibDOTrusDOTec
only problem with using Python is I don't know an easy way to render TeX to an OpenGL context, so without an investment in that facility you'd have to settle for ASCII Fitch derivations
with JavaScript you could use HTML tables and MathJax
if you added about 10 pages of intro and definitions and some example code and derivations, any CS retard in a decent undergrad program could knock this out in a couple of weeks, probably less than 5 days for most
only problem is the design isn't very well specified so you'd have to spend several hours doing a close reading, which is more of a /lit/ skill
all of those details and snags would be fixed and sanded off during curriculum development
