Hacker News Reader

Comment by muldvarp | Hacker News Reader

> However, the only reason it verifies is we haven't yet implemented `||`

You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.

> We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.

You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.

View on HN

> You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.

You're right. We should. (We will be adding this as we are able.)

> You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.

A 7-point blog post is hardly "long-form" :)

But more to the point, Rust has already achieved this "interface formality", as we state in the second paragraph of this "long-form" piece. That achievement on the part of Rust is indeed groundbreaking. Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?

Fair enough. We have a much more generous definition of "working prototype" than you do. Hopefully one day soon we'll have something that clears yours.

> Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?

You're not replicating what Rust does, you're replicating what Frama-C does.

Then again, even just replicating what Rust does would be extremely difficult (if not impossible) given the pervasiveness of undefined behavior in C.

> Fair enough. We have a much more generous definition of "working prototype" than you do.

How many useful C programs do you know that require no loops and no binary operators?

> Xr0 1.0.0 will enable programming in C with no undefined behaviour, but for now it's useful for verifying sections of programs.

Literally on the website. The purpose of the prototype is to show the feasibility of the approach we've taken, not to work on whole programs.

> The purpose of the prototype is to show the feasibility of the approach we've taken

But it doesn't do that. You haven't shown that this approach is able to deal with loops and loops are pretty fundamental to every C program.

Heck, you haven't technically shown that this approach can deal with binary operators. I would love to turn Xr0 into an improptu SAT solver, but without `&&` and `||` that sadly isn't possible right now.

You missed the `!=`, `==` (in many instances), bitwise operators, recursion and `goto`. (And much, much more.)

Xr0 is a work in progress, and we'll get there step-by-step.

Yes, the subset of C it currently supports is so small I'm really puzzled what you think this prototype is proving. That you can parse C?

It's even less impressive than that. That we can parse a subset of C. That's all there is to see here.

Then why not write a blog post "We can parse C" instead of "Xr0 makes C safe (it doesn't actually and we are unable or unwilling to go into details and also please don't ask us about Frama-C)"?

Shouldn't it be called "We can't parse C" since we can only parse a trivial subset of it?

Reply on news.ycombinator.com