3 ms·
Wow, that looks like a killer feature for .Net I will definitely steal some ideas from Coyote to drive Nim formally verification story of concurrent code forwa
by mratsim 6y ago
Wow, that looks like a killer feature for .Net
I will definitely steal some ideas from Coyote to drive Nim formally verification story of concurrent code forward.
On the Rust side, i feel like Loom has a lot of potential https://github.com/tokio-rs/loom https://github.com/tokio-rs/loom and I'm keeping tabs on them.
- inaseer 6y agoLooms looks quite interesting and is similar to Coyote in a lot of ways. The exploration engine used by Coyote is based on years of investigation by Microsoft Research so it scales nicely on real world programs. I believe the Coyote team is looking into exposing the systematic exploration capabilities in a language and platform agnostic way so developers can create language-specific bindings in their language of choice and benefit from all the research done over decades. No timelines that I'm aware of but it is on the road map I believe.
- mratsim 6y agoYes I'm in the middle of many Microsoft papers[1] to add model checking to Nim, in particular CHESS.[2] [1]: https://github.com/mratsim/weave/issues/18 https://github.com/mratsim/weave/issues/18 [2]: Finding and Reproducing Heisenbugs in Concurrent Programs, http://www.cs.ucr.edu/~neamtiu/pubs/osdi08musuvathi.pdf http://www.cs.ucr.edu/~neamtiu/pubs/osdi08musuvathi.pdf