I understand. Probably for very simple formulas (and trivial mistakes it could work). Note however that it is not an “hobby” project and the effort to put into that vs. its usefulness is questionable. Probably it will be able to catch simple mistakes, but not less obvious ones, and therefore is useless for a professional mathematician, and harmful for a non-professional one since it will allow you to be less careful in what you are doing. Just a different kind of project, not really an extension of TeXmacs. I do not see how this would make WYSIWYG more compelling since a similar system can certainly work for math entered in LaTeX (modulo weird macro definitions).