C0 is used in 15-122, Carnegie Mellon's second semester introductory programming class. I am currently taking this class. The class teaches C0 for the first two thirds of the semester and then transitions to C for the final part of the semester.

C0 has essentially the same syntax as C, but for pedagogical purposes the semantics of the language have been changed to be much more similar to java. Instead of manual memory management, there is a garbage collector, and user defined structs can only be allocated on the heap. Additionally, there is only one integer type which is a signed 32-bit two's complement integer. Overflow is defined as wrapping. strings are opaque immutable types implemented at a language level, rather than just null-terminated buffers. C0 catches out of bounds array accesses at run time. While C0 internally stores array lengths to perform this check, the length is not accessible from C0 code so array lengths must be passed around just the same as C.

C0's biggest feature beyond C is that it allows for contracts. Functions can have preconditions and postconditions. There are also loop invariant contracts and assertions. These contracts are checked at run time when specific flag is passed to the compiler or interpreter (C0 has both, and uses a bytecode internally). A major focus of the class is proving the safety and correctness of the programs we write using these contracts. We are encouraged to prove safety and correctness using only logical reasoning from contract to contract, not operational reasoning. A co-requisite of the class is a course in proofs. There seems to be a heavy influence on the teaching style from Dijkstra's "On the cruelty of really teaching computing science" [1].

The 15-122 class has written assignments focusing on the proofs part of the course and programming assignments which for the most part are automatically graded by autolab [5]. Our code is tested against a number of unit tests to ensure its correctness and our contracts are also tested to see if they can catch bugs in faulty implementations.

C0's implementation is not open source, but it appears to be used in ongoing research [2]. Here is the language website and course website [3], [4].

[1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD103...

[2] http://www.cs.cmu.edu/~fp/papers/cc016.pdf

[3] http://c0.typesafety.net/

[4] http://www.cs.cmu.edu/~15122/

[5] http://www.autolabproject.com/