@nbspnbsp @bitemyapp @steshaw @runarorama Use a richer type system and it can convey the laws.
-
-
Replying to @pdxleif
@pdxleif@nbspnbsp@bitemyapp@steshaw@runarorama On the other hand you then _must_ prove the laws, which can be tedious.1 reply 0 retweets 0 likes -
Replying to @d_christiansen
@d_christiansen or have cake & eat it! Remind me how to ask Idris to "believe me"? /cc@pdxleif@nbspnbsp@bitemyapp@runarorama2 replies 0 retweets 0 likes -
Replying to @steshaw
@steshaw@d_christiansen@nbspnbsp@bitemyapp@runarorama A postulate has a type but no value (so it doesn't reduce).1 reply 0 retweets 0 likes -
Replying to @pdxleif
@pdxleif Can you run a program that has "hand waved" proofs using postulate /cc@d_christiansen@nbspnbsp@bitemyapp@runarorama3 replies 0 retweets 0 likes -
Replying to @steshaw
@steshaw@d_christiansen@nbspnbsp@bitemyapp@runarorama You can lie all you want, as long as it's not in stuff referenced at runtime.1 reply 0 retweets 1 like -
Replying to @pdxleif
@pdxleif@d_christiansen@nbspnbsp@bitemyapp@runarorama Thanks. The word "lie" is such a strong word, would prefer to find another… ideas?3 replies 0 retweets 0 likes -
Replying to @steshaw
@pdxleif like `fabricate`, `fudge` & `hope`. Rejected the short `fib` as it might actually be true or taken for Fibonacci. /cc@edwinbrady1 reply 0 retweets 0 likes
-
-
Replying to @edwinbrady
@edwinbrady@pdxleif Sorry, I hadn't seen `postulate` and didn't realise it was built in — added in Idris in 0.9.6 http://www.idris-lang.org/idris-0-9-6-released/ …0 replies 0 retweets 0 likesThanks. 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.