9 ms·

If anything it's rust attempt to appease C++ programmers that caused this dilemma. Both have too much complexity for verified correctness.

by j-pb 5y ago

pcwalton 5y ago
In reality, the #1 thing that helps to verify correctness, if that if what you are after, is memory safety, something Rust has and Zig does not. In fact, in one common PL sense, a language that is not memory safe cannot be "verified correct", because what people usually mean by "verified correct" is type safety proofs, and obviously you can't prove a language type-safe if it isn't type-safe.
- j-pb 5y ago
  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.
  - pcwalton 5y ago
    I think you'll find that if you want to prove a program correct (which vanishingly few people really do in practice, but anyway) you will find it infinitely easier to do so if the language it's written in is type- and memory-safe. Even if you're talking about the looser notion of "does my program behave correctly", we have a lot of evidence that using simpler unsafe languages doesn't produce more correct programs than more complex safe languages. See: basically every piece of C code in the wild.

If anything it's rust attempt to appease C++ programmers that caused this dilemma. Both have too much complexity for verified correctness.

by j-pb 5y ago

If anything it's rust attempt to appease C++ programmers that caused this dilemma. Both have too much complexity for verified correctness.

pcwalton 5y ago

In reality, the #1 thing that helps to verify correctness, if that if what you are after, is memory safety, something Rust has and Zig does not. In fact, in one common PL sense, a language that is not memory safe cannot be "verified correct", because what people usually mean by "verified correct" is type safety proofs, and obviously you can't prove a language type-safe if it isn't type-safe.

j-pb 5y ago
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.
- pcwalton 5y ago
  I think you'll find that if you want to prove a program correct (which vanishingly few people really do in practice, but anyway) you will find it infinitely easier to do so if the language it's written in is type- and memory-safe. Even if you're talking about the looser notion of "does my program behave correctly", we have a lot of evidence that using simpler unsafe languages doesn't produce more correct programs than more complex safe languages. See: basically every piece of C code in the wild.