[pcwalton]

For one, it doesn't do all the "memory safety parts", according to the readme. I'm very skeptical that Zig can be made memory safe with a checker while still remaining compatible with existing code. Certainly neither C nor C++ can, and Zig isn't meaningfully different in expressivity (if anything, it's more expressive, which is the opposite of what you want).

[throwawaymaths]

FTrepo:

Q: You didn't do X, so Zig will never be able to track X

A: Maybe. Only way to know for sure is to fork this (or, hopefully, a 'real' successor) and fail. However, consider that "trivially" it should be possible to externally annotate every zig file with lifetime/type annotations identical to that of Rust and run "exactly the same" analysis as Rust and get the same memory safety as Rust.

it appears the clr author anticipated you: you didnt fork it, try, and fail, so you have ceded the authority to credibly make your speculative complaint

> Zig isn't meaningfully different in expressivity

it is meaningfully different in expressivity at the AIR level. AIR looks nothing like c, c++, zig, or rust.

[Ygg2]

> it appears the clr author anticipated you: you didnt fork it, try, and fail, so you have ceded the authority to credibly make your speculative complaint

That's a caveat. Not an expectation.

Plus that's not how proof works. Neither Zig nor Zig+Clr have really proven they are safe, ergo they are unsafe or possibly safe (respectively).

[throwawaymaths]

wow what are you afraid of. you're working really hard to tear down something that is an incomplete proof of concept.

[zamalek]

The original argument is that clr proves Zig is as safe as Rust, per your wording " all the memory safety parts."

Does the incompletely POC do all the parts, or doesn't it? That is no criticism against the project itself, striving to improve memory safety in any language is an honorable goal. The cinch is that an incomplete POC doesn't prove things one way or another, the POC needs to be completed (or at least completed far enough to prove your point). It either matches or exceeds Rust memory safety, or it only vastly improves Zig memory safety. Both are great outcomes, for what it's worth.

It shouldn't have been shown as an example of how Zig is just as/more safe than Rust if it is not. Mispresenting the project tears it down, not questioning its use an an example. Just like misrepresenting Zig's safety (and Rust's unsafety) tears Zig down.

[throwawaymaths]

I guess the question is what level of satisfied are you.

Are you satisfied like "proof is left as an exercise for the reader" in a math textbook? Or is it like "I have proved this but it's too large to fit in the margins"?

It seems author couldn't be bothered to complete it since there's (minor) missing features in the zig compiler that need to be satisfied first to make it worthwhile?

[zamalek]

> Are you satisfied like "proof is left as an exercise for the reader" in a math textbook? Or is it like "I have proved this but it's too large to fit in the margins"?

In the first example the proof would be available elsewhere. In the second example, no. My answer is "just the facts as they exist today."

A mathematical proof holds no inherent utility. The thing it proves is what is useful. What I find useful is not suffering memory safety woes. Can I run a tool, any tool, today that will give me the same assurances that the Rust compiler (and/or Miri) does? Conjecture about the future is pointless because someone could equally go and write some static analysis tool like clr for Rust to fix all the bad parts, or fix the compiler, or the parts of clr that aren't finished might be impossible (we don't know, nobody has tried), or the heat death of the universe could come early. All still irrelevant, because I'm a user and I care exclusively about what I can currently do.

[Ygg2]

Nothing, it's the principle of the thing. I.e. when you make a challenging to evaluate statement, the burden of proof is on the one making the claim.

If I say "Moon is made of millennia old cheese", the burden of proof isn't on you to go create a rocket, fly to the moon, sample it and come with conclusions, but on me, making a difficult to verify statement.

[throwawaymaths]

the author has put a lot of unpaid I'm guessing work into this repo -- seems reasonable for the author to demand a bit of work out of any asshole taking a potshot at it.