We are implementing the Red JonPRL proof assistant (https://github.com/JonPRL/sml-red-jonprl https://github.com/JonPRL/sml-red-jonprl) in SML (using MLton for b

We are implementing the Red JonPRL proof assistant (https://github.com/JonPRL/sml-red-jonprl https://github.com/JonPRL/sml-red-jonprl) in SML (using MLton for builds and SML/NJ for development), and could hardly be happier. Dealing with unicode is a pain, but so far, we've been able to do what we need.