ineol1

Derek Dreyer and collaborators are working on specifying what needs to be proven about unsafe code, see http://plv.mpi-sws.org/rustbelt/

To 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.

Given his support of GamerGate (http://matthewhopkinsnews.com/?cat=64) I don't really think his opinion on this matter are very fair and balanced...

Isn't Coq's language, Gallina, not Turing complete (all functions must terminate)? It's still a programming language.

It's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.

It'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...