I'm not sure what role you envision for C0 in combination to TLA
We might think of a sort of TLAPLUS0. We would use TLC and PLUSCAL.
No TLAPS, no temporal logic and no translation of the PLUSCAL algorithm
into TLAPLUS macros.
The purpose would be to teach that expressing an algorithm using mathematical
concepts: relations, functions, set builder notation is more interesting than a
language to design an algorithm.
Then the transition of TLAPLUS0 to the rest of TLAPLUS would be easy.
--
FL