ineol1·10 ปีที่แล้ว·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 ปีที่แล้ว·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 ปีที่แล้ว·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 ปีที่แล้ว·discussIsn't Coq's language, Gallina, not Turing complete (all functions must terminate)? It's still a programming language.
ineol1·11 ปีที่แล้ว·discussIt's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.
ineol1·12 ปีที่แล้ว·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...