PL/CS is an instructional dialect of PL/I. It is defined by selection features of PL/I, and then restricting the manner in which those features can be used. The implementation is an error-repairing compiler based on PL/C, in which error-repair is carried to the point where a user is deliberately encouraged to use an abbreviated entry syntax and rely on the compiler to expand this to produce a complete, PL/I-compatible program. PL/CS also includes an "assertion" facility that can be used either as a conventional diagnostic tool, or as the basis of a formal proof of correctness in a logical system provided within the language.