@edwinbrady Idris looks impressive. One question though: how do you approach the problem of Int overflowing?
@andreasdotorg the language itself doesn't worry, but if it's important you can add a proof that an Int is bounded
-
-
@edwinbrady And by "all of the time" I mean "every time an Int is used as an index into a buffer". -
@andreasdotorg Ah - I don't use ints to index into lists... see https://github.com/edwinb/Idris-dev/blob/master/lib/prelude/vect.idr … for example - 3 more replies
New conversation -
-
-
@edwinbrady For system level programming, it is important just about all of the time. Int overflows are #1 reason for security bugs. -
@andreasdotorg This has something to say, but I haven't de-bitrotted the code for the latest version yet: http://www.cs.st-andrews.ac.uk/~eb/writings/plpv11.pdf … - 1 more reply
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.