The plan makes sense. A likely issue for folks currently preparing papers in LaTeX is that they will be put off by the extra work of having to port/write another copy of their document in Nota, but maybe this is intended. You shouldn't just be dumping your paper to the web.

Re documents that would be useful, you could dogfood Nota with 242 to show how powerful it could be to teach students PL theory. A course like 15-312 would be much less intimidating for students if materials were encoded both informally/formally in Nota. You could imagine porting one chapter from PFPL as a small example.

I'm teaching a new course on algorithms in the spring and I plan to try it out to develop some online course materials. Will get in touch with you with any questions / to share what we prototype. You might also want to share this with Umut who has been developing (what I believe is) a KaTeX-based system called Diderot that a lot of CMU courses are using now.