Why Dependently Typed Programming Will (One Day) Rock Your World http://ejenk.com/blog/why-dependently-typed-programming-will-one-day-rock-your-world.html …
-
-
Replying to @bitemyapp
@bitemyapp@pozorvlak Presumably proof(b!=0) would be processor dependent, thus nullifying a major benefit of high level languages?1 reply 0 retweets 0 likes -
Replying to @drgeraint
@drgeraint@bitemyapp I've only seen it with bigints, where proofs are portable; not sure about floats in DT languages /cc@edwinbrady1 reply 0 retweets 0 likes -
Replying to @pozorvlak
@pozorvlak@drgeraint@bitemyapp we have the usual float types, but I find it hard to get excited about catching this sort of thing tbh...1 reply 0 retweets 1 like -
Replying to @edwinbrady
@edwinbrady@pozorvlak@drgeraint there are some cranky embedded engineers out there.1 reply 0 retweets 0 likes -
Replying to @bitemyapp
@bitemyapp@edwinbrady@pozorvlak@drgeraint I originally wrote the post with ints instead of floats. Should’ve kept it that way.2 replies 0 retweets 0 likes
@ejenk Making a small example that's also convincing and interesting is always hard, of course. @bitemyapp @pozorvlak @drgeraint
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.