To quote from Dijkstras essay "On the cruelty of really teaching computing science". > Right from the beginning, and all through the course, we stress that the

To quote from Dijkstras essay "On the cruelty of really teaching computing science". > Right from the beginning, and all through the course, we stress that the programmer's task is not just to write down a program, but that his main task is to give a formal proof that the program he proposes meets the equally formal functional specification. While designing proofs and programs hand in hand, the student gets ample opportunity to perfect his manipulative agility with the predicate calculus. Finally, in order to drive home the message that this introductory programming course is primarily a course in formal mathematics, we see to it that the programming language in question has not been implemented on campus so that students are protected from the temptation to test their programs. And this concludes the sketch of my proposal for an introductory programming course for freshmen. There are more ways to proof correctness than through the type system alone. Would I prefer Zig to have a strong type system? Absolutely, but the reason why I choose Zig as a comparator is not because I feel that it does a significantly better Job at correctness than Rust, neither do fully. (And if I had to build something verifiably correct I'd probably Idris with linear types or something.) But I feel that with Zig I'd at least have the chance to proof the correctness of my program manually (with pen & paper). Although Zig is still heavily in flux it's simple and focused enough that it "being done", and me thus being able to understand it in its entirety, is at least visible on the horizon. With Rusts complexity that date is much further out into the future, if it is ever achievable. And even then, I'm not sure that I could fit enough of the Rust language and std into my head to be satisfied with the correctness of my proofs. Nor am I convinced that it can fit into the compiler devs heads sufficiently to ensure that the compiler is behaving correctly.