I haven't tried it yet, but there is a PlusCal-to-Go compiler now: https://distcompiler.github.io/ https://distcompiler.github.io/ I have no idea how well it w

I haven't tried it yet, but there is a PlusCal-to-Go compiler now: https://distcompiler.github.io/ https://distcompiler.github.io/ I have no idea how well it works, but it seems pretty interesting. I do think that that's something a bit more compelling about something like Isabelle, which offers first-class support for exporting programs that can be directly executed, which in theory would inherit all the proofs for the parent Isabelle (though that's not strictly true).