3 ms·
Yes, it's quite cool. The specification is a literate Julia program and the specification document is built from it. Simultaneously, they run large scale simula
by KenoFischer 9y ago
Yes, it's quite cool. The specification is a literate Julia program and the specification document is built from it. Simultaneously, they run large scale simulations to make sure that the specification behaves as the theory says it should. There was some discussion with them about deployment, and they funded us for a proof of concept Julia-to-C compiler, but the continuation of that discussion is probably still a number of years off. It's a very long term project.
- skybrian 9y agoHaving read a little about TLA+ recently, I'm curious about how specifications are written in Julia. (For example, is there model-checking involved?)
- simonbyrne 9y agoThere was a talk at JuliaCon 2015: https://www.youtube.com/watch?v=19zm1Fn0S9M https://www.youtube.com/watch?v=19zm1Fn0S9M Slides here: http://juliacon.org/2015/images/juliacon2015_moss_v3.pdf http://juliacon.org/2015/images/juliacon2015_moss_v3.pdf