4 ms·
The problem with TLA+ is that you still have to hand translate your solution to C++/C#/Java/… Using Dafny (for example) gives you the advantages of TLA+ combin
by mbrodersen 4y ago
The problem with TLA+ is that you still have to hand translate your solution to C++/C#/Java/…
Using Dafny (for example) gives you the advantages of TLA+ combined with proven correct running code.
- gmfawcett 4y agoDafny is cool, but I believe they tackle different problem spaces. For example, how would you verify a distributed algorithm with Dafny?
- mbrodersen 4y agoYou absolutely can. TLA+ is basically a state transition system. Something you can write in Dafny and prove correct using its Refinement types. And the end result is running software you can drop right into production.
- hwayne 4y agoCheck out IronFleet! https://www.microsoft.com/en-us/research/wp-content/uploads/2015/10/ironfleet.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
- gmfawcett 4y agoThanks, Hillel. I brought a speculation to a citation fight -- I'm glad you won :) Seriously, this is a very interesting read.