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