@propensive Not a fan of type-driven design? :-)
-
-
-
@oxnrtr It's terrible! Why would you choose the hassle of types when you can just cover everything with simple tests? ;) - Show replies
New conversation -
-
-
@psnively@propensive@oxnrtr Yes, and also the types we define must be tested to ensure they actually keep the promises we then rely on.Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@psnively@propensive@oxnrtr I gave an example at ScalaDays: I create a Pos type that promises to never hold a non-positive integer. -
@psnively@propensive@oxnrtr The type checker will ensure only a Pos is passed to methods that take Pos, not that the integer is positive.
End of conversation
New conversation -
-
-
@psnively@propensive@oxnrtr Yes, and here's part of the reason why: https://github.com/milessabin/shapeless/blob/master/core/src/test/scala/shapeless/nat.scala …Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@psnively@propensive@oxnrtr Is coq written in coq such that it proves itself correct? Or do we trust its proofs because coq is tested?Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@psnively@propensive A self-verifying theorem proover is interesting. Seems like anything could declare itself a correct theorem proover.Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.