ineol1·vor 10 Jahren·discussDerek Dreyer and collaborators are working on specifying what needs to be proven about unsafe code, see http://plv.mpi-sws.org/rustbelt/
ineol1·vor 11 Jahren·discussTo give more context, B. Pierce, one of the authors of the Dropbox paper is (one of?) the main author of Unison, and also coauthor of the paper you linked.EDIT: The parent cited http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf by Pierce in 2004, where the authors stressed the difficulty of writing a specification for a file synchronizer, in this case Unison.
ineol1·vor 11 Jahren·discussGiven his support of GamerGate (http://matthewhopkinsnews.com/?cat=64) I don't really think his opinion on this matter are very fair and balanced...
ineol1·vor 11 Jahren·discussIsn't Coq's language, Gallina, not Turing complete (all functions must terminate)? It's still a programming language.
ineol1·vor 11 Jahren·discussIt's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.
ineol1·vor 12 Jahren·discussIt's their PR photos. There are these too (and many more on that blog) : http://universiteenruines.tumblr.com/image/103057236913 http://universiteenruines.tumblr.com/post/104835621673/nosta...