3 ms·

perhaps I'm missing the intent, but would it be feasible to have formal verification specifications like with TLA+ act as a blueprint for generating machine cod

by fire 4y ago

perhaps I'm missing the intent, but would it be feasible to have formal verification specifications like with TLA+ act as a blueprint for generating machine code? It would be fairly cool to be able to design a system using tools like this and have a way to translate it without the possibility of introducing errors during translation to code. Perhaps what I'm thinking is more automatic generation of test cases? But I'm not quite sure what my brain is trying to watch onto here.

hwayne 4y ago
The universal problem is "generating code from a formal spec" is extremely, maddeningly, pull-your-hair-outingly hard. A slightly easier thing, as you said, generating test cases, which is what the Mongo people have been advancing: https://arxiv.org/abs/2006.00915 https://arxiv.org/abs/2006.00915 (Another interesting approach in this space is P, which is lower-level than TLA+ but also can compile to C#: https://github.com/p-org/P https://github.com/p-org/P)
- inaseer 4y ago
  Check out Coyote (which is an evolution of P) and allows you to "model check" .NET code to find hard to find race condition-y bugs in your implementation. We have used it very successfully on a number of projects at Microsoft. I should probably do more public talks on it to get the word out. Finding subtle bugs in your implementation using tools like Coyote is easier than most people realize.
  - inaseer 4y ago
    TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implemention.
- zokier 4y ago
  Aren't F* and Dafny kinda also solving this problem of bridging the gap between formal spec and executable code? Another interesting question is if there are gaps between the abstract systems-level specs of TLA and the relatively low-level specs of F* that might need bridging?
zozbot234 4y ago
TLA+ is not an end-to-end system. You're not necessarily verifying your final code, most of the time you're only building a "toy" model of your high-level design and verifying that. So generating code from the model would not be helpful.
gjadi 4y ago
I don't remember the details, but I remember some people where comparing traces of execution between the program and the TLA+ code. If the traces don't match, you've got a problem.

by fire 4y ago

hwayne 4y ago

The universal problem is "generating code from a formal spec" is extremely, maddeningly, pull-your-hair-outingly hard. A slightly easier thing, as you said, generating test cases, which is what the Mongo people have been advancing: https://arxiv.org/abs/2006.00915 https://arxiv.org/abs/2006.00915 (Another interesting approach in this space is P, which is lower-level than TLA+ but also can compile to C#: https://github.com/p-org/P https://github.com/p-org/P)

inaseer 4y ago
Check out Coyote (which is an evolution of P) and allows you to "model check" .NET code to find hard to find race condition-y bugs in your implementation. We have used it very successfully on a number of projects at Microsoft. I should probably do more public talks on it to get the word out. Finding subtle bugs in your implementation using tools like Coyote is easier than most people realize.
- inaseer 4y ago
  TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implemention.
zokier 4y ago
Aren't F* and Dafny kinda also solving this problem of bridging the gap between formal spec and executable code? Another interesting question is if there are gaps between the abstract systems-level specs of TLA and the relatively low-level specs of F* that might need bridging?

zozbot234 4y ago

TLA+ is not an end-to-end system. You're not necessarily verifying your final code, most of the time you're only building a "toy" model of your high-level design and verifying that. So generating code from the model would not be helpful.

gjadi 4y ago

I don't remember the details, but I remember some people where comparing traces of execution between the program and the TLA+ code. If the traces don't match, you've got a problem.