“I am currently a TA for 15-122 at Carnegie Mellon, the class that C0 was originally made for. I would argue that C0 does an excellent job at breeding good programmers because of the following features:
1. Contracts in C0 bake preconditions, post conditions, and loop invariants right into the language. Contracts are only checked when in "dynamic recompilation" mode (basically debug mode). This allows you to check the correctness of your code more easily (and, importantly, in an easily gradable way).
2. The language is designed in such a way to introduce C to programmers that are used to other higher level languages. In the C0 phase of the course we introduce students to fundamental concepts like memory allocation, code reasoning and contracts, binary representations of numbers, and unit testing. Next we transition to C1 (included in the C0 install) which introduces typedefs and other features of C. At this point we focus on introducing data structures. Finally we make the final transition to C, where we talk about undefined behavior, gcc, stack vs heap, etc.
I've taken this course myself, and I would argue that this measured approach to learning C is far superior to throwing students (most of whom have no low-level programming experience) straight into C.”
The course that uses C0 goes on later to C, and is literally titled “Principles Of Imperative Computation”. We use Standard ML for “Introduction to Functional Programming”.
(As an aside nearly every language defines division on the set of integers this way so it’s not even like we’re making this up)