I realised that, as Pascal might put it Cyclone is a C like language designed to ensure that programs are correct. I saw it as a related form of safety others might be interested in.

I already posted on Clight & CompCert which is much more salient in terms of ensuring compiler correctness and a safe subset that falls within the scope of the verified compiler's correctness.