The course it was made for at CMU (15-122) is primarily about writing contracts for imperative programs, I guess they decided C0 was the best way to do that since students have to take C anyway in 15-213 afterwards. Robert Harper's blog he apparently pushed for freshmen to land directly in a SML course where they would learn both imperative and functional methods but for legacy reasons they all agreed C should still be taught but with an emphasis on correctness/contracts so C0 was born.