ineol1

4 ms·

1. 1.▲
   by ineol1 10y ago

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

   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/paper
3. 3.▲
   by ineol1 11y ago

   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...
4. 4.▲
   by ineol1 11y ago

   Isn't Coq's language, Gallina, not Turing complete (all functions must terminate)? It's still a programming language.
5. 5.▲
   by ineol1 12y ago

   It's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.
6. 6.▲
   by ineol1 12y ago

   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/no