Comment by jwpapi

12 hours ago

I’m missing an actual explanation of how that works.

I feel like we all had the idea, but how is all possible move sequences proven ?

What if the possible scenarios are too big to proof or test.

Like on a 2 dimensional game it’s easy, but you could make it multidimensional and introduce an unlimited amount of special rules, (if on a prime number dimension on 3 but not more prime numbers you are allowed to jump to another prime numbers with 3 but not less coordinates)

How is bend protecting it? I was checkin github and the paper, but I was not motivated enough. I feel like an actual explanation of how proofing works is missing.

For Lean I understand how it works, here not.

2 comments

jwpapi

Reply
LightMachine  12 hours ago

You can prove infinitely many cases by induction.

It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove that, assuming the property holds for N, it also holds for N+1; then, you can conclude the property holds for every N, up to infinity. This is a bit of a mouthful, but the logic holds.

Induction is the one trick that makes all of mathematics (as we know it) possible, and it also applies to software. So, for example, to prove that no move leads to an invalid state, we prove that the initial state is valid, and then prove that, given a valid state, applying any event won't return an invalid state.

And that's it actually.

Of course, once you have an app with hundreds of actions, proving that no action leads to an invalid state requires a lot of these "induction arguments". But not infinitely many, because there is a finite amount of "infinite paths" that a real software can take. So, that's what the AI does. It proves, by induction, that none of these "infinite paths" that an app can take leads to an invalid state. And this convinces the compiler that invalid states are impossible.

Theorem proving in Bend is a dance between the prover (the model) and the compiler (the checker); a machine trying to convince another machine about properties of infinite states. And that's is kinda poetic, don't you think?