4 ms·

How would I prove to the client that the implementation conforms to the model? Wouldn't it end up being written in some crappy programming language for which no

How would I prove to the client that the implementation conforms to the model? Wouldn't it end up being written in some crappy programming language for which no one can agree on a formal semantics anyway, running on some grotesquely complicated processor family full of defects and bugs?

nivertech 5y ago
The model is to prove your design, not the implementation. There is no reason to start implementing things, if your design is wrong. Formal Specification proves your design, while Formal Verification proves your implementation. As far as I understand this project - Stateright does both (i.e. 2-in-1). Kind of executable model?
- jonnadal 5y ago
  Regarding the last point — correct, Stateright aims to verify both. It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…). Examples: SD Paxos: https://github.com/stateright/stateright/blob/master/examples/paxos.rs https://github.com/stateright/stateright/blob/master/example... ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/examples/linearizable-register.rs https://github.com/stateright/stateright/blob/master/example...
hwayne 5y ago
We've been working on some techniques for this. To my understanding, Stateright (the OP's repo) directly connects the spec with Rust code, so you can make some implementation guarantees. If you don't have that (say you're using TLA+), one really promising technique is to generate behavioral traces and then refine those into code tests. I know a few companies have done this successfully, and I've been working on some examples of how it's done, but to my knowledge there's no battle-tested tooling that do this automatically. It's all bespoke for now.
- faeyanpiraat 5y ago
  Wow, these formal specification tools is something I always wanted to look into but the learning curve seems steep. Having a specification which is guaranteed to be correct before implementation begins is a programmer’s wet dream.
  - hwayne 5y ago
    > Wow, these formal specification tools is something I always wanted to look into but the learning curve seems steep. One of my dreams is to flatten that learning curve. I don't think we'll ever make these tools effortless, but I think it's possible to reach a point where "these tools are too hard to learn" isn't a barrier anymore. (Even then, I imagine a lot of people will learn some formal specification, and think "this isn't useful for me", and never touch them again. And that's fine. But I want anybody to be able to reach the point where they can make that decision, as opposed to feeling like they're locked out by default. We have a long way to go, but I think we're considerably further along than we were five years ago.) > Having a specification which is guaranteed to be correct before implementation begins is a programmer’s wet dream. I wouldn't say guaranteed to be correct, but at least it's, like, closer to correct? Less likely to have horrific bugs, or bizarre edge cases in the requirements that nobody notices until neck deep into the implementation. Stuff that increases founded confidence.

nivertech 5y ago

The model is to prove your design, not the implementation. There is no reason to start implementing things, if your design is wrong. Formal Specification proves your design, while Formal Verification proves your implementation. As far as I understand this project - Stateright does both (i.e. 2-in-1). Kind of executable model?

jonnadal 5y ago
Regarding the last point — correct, Stateright aims to verify both. It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…). Examples: SD Paxos: https://github.com/stateright/stateright/blob/master/examples/paxos.rs https://github.com/stateright/stateright/blob/master/example... ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/examples/linearizable-register.rs https://github.com/stateright/stateright/blob/master/example...

hwayne 5y ago

We've been working on some techniques for this. To my understanding, Stateright (the OP's repo) directly connects the spec with Rust code, so you can make some implementation guarantees. If you don't have that (say you're using TLA+), one really promising technique is to generate behavioral traces and then refine those into code tests. I know a few companies have done this successfully, and I've been working on some examples of how it's done, but to my knowledge there's no battle-tested tooling that do this automatically. It's all bespoke for now.

faeyanpiraat 5y ago
Wow, these formal specification tools is something I always wanted to look into but the learning curve seems steep. Having a specification which is guaranteed to be correct before implementation begins is a programmer’s wet dream.
- hwayne 5y ago
  > Wow, these formal specification tools is something I always wanted to look into but the learning curve seems steep. One of my dreams is to flatten that learning curve. I don't think we'll ever make these tools effortless, but I think it's possible to reach a point where "these tools are too hard to learn" isn't a barrier anymore. (Even then, I imagine a lot of people will learn some formal specification, and think "this isn't useful for me", and never touch them again. And that's fine. But I want anybody to be able to reach the point where they can make that decision, as opposed to feeling like they're locked out by default. We have a long way to go, but I think we're considerably further along than we were five years ago.) > Having a specification which is guaranteed to be correct before implementation begins is a programmer’s wet dream. I wouldn't say guaranteed to be correct, but at least it's, like, closer to correct? Less likely to have horrific bugs, or bizarre edge cases in the requirements that nobody notices until neck deep into the implementation. Stuff that increases founded confidence.