It doesn't look bad versus regular C. You still have the C-specific risks in the module and at module interfaces that other language reduce. It's also harder to parse, analyze, and compile in a secure way. With SPARK & formal tools, one can get a strong analysis that the code will always meet the spec. The ability to fully do that for C has only come online in the past few years. It appears to take more work, too.