3 ms·

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

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

by hwayne 5y ago

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.