top | item 39978374

(no title)

akiarie | 1 year ago

> 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.

discuss

order

muldvarp|1 year ago

> 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.

akiarie|1 year ago

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.