Try JonPRL

[markfarrell]

It would be nice to be able to try out JonPRL in the web browser, e.g. like Try PureScript.

[jonsterling]

That would be so cool! I believe that MLKit has this "SML to JS" thing that we could use. However, currently JonPRL is only compatible with SML/NJ, but Red JonPRL will be fully Definition-compliant, and so we should be able to build it with MLKit.

Another option that would be possible today, I suppose, is to just throw a JonPRL executable onto a server somewhere and have the web app shell out to it.

In fact, in addition to just having "Try JonPRL" (which is great PR), I'd love to have some kind of web-based interface that people might actually use for real stuff.

[markfarrell]

Yeah, as for a web-based interface: do you think it would be possible / a good idea to have a notebook-style interface where e.g. theorems would be the inputs to cells and program extracts would be outputs?

[jonsterling]

@markfarrell I love that idea... Maybe it would be possible to integrate with that IPython Notebook thing or something?

[jozefg]

(Chiming in here) This sounds really slick! As a (distant) project I also don't see any significant technical challenges in translating JonPRL's realizers into just plain old javascript.. Could be an interesting follow up if this project works out

[markfarrell]

In addition to that thought, is there any way to make a (web-based) editor for JonPRL that, when trying to prove a theorem, would bring up suggestions for tactics and lemmas I could be allowed to use to achieve a goal?