ineol1·10 anni fa·discussDerek Dreyer and collaborators are working on specifying what needs to be proven about unsafe code, see http://plv.mpi-sws.org/rustbelt/
ineol1·11 anni fa·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·11 anni fa·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·11 anni fa·discussIsn't Coq's language, Gallina, not Turing complete (all functions must terminate)? It's still a programming language.
ineol1·11 anni fa·discussIt's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.
ineol1·12 anni fa·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...