@samth @bitemyapp @puffnfresh @djspiewak I look forward to it. Please link?
-
@dibblego@cartazio@puffnfresh@djspiewak@bitemyapp b/c sometimes the work to convince a computer that the code is right isn't worth it.
@samth @cartazio @puffnfresh @djspiewak @bitemyapp What is an instance of that? All instances I have seen are so far lacking imagination.
-
-
@dibblego@samth@puffnfresh@djspiewak@bitemyapp try writing an imperative program in coq. sometimes too much types is bad. -
@cartazio@samth@puffnfresh@djspiewak@bitemyapp Do you mean, sometimes I want to specify part of my proof and not the whole proof?
End of conversation
New conversation -
-
-
@dibblego@cartazio@puffnfresh@djspiewak@bitemyapp Two examples: a garbage collector; the code in fig. 1 of http://www.ccs.neu.edu/racket/pubs/oopsla12-tsdthf.pdf … -
@dibblego@cartazio@puffnfresh@djspiewak@bitemyapp Of course, we wrote that paper on types for the second, but that's _lots_ of work.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.