Use Idris then. This is why multiple languages exist; there are tradeoffs and you have to compromise.
-
-
Replying to @ManishEarth @fugueish
Having to prove all your invariants is a *major* tradeoff that would likely make Rust a much more niche language.
1 reply 0 retweets 0 likes -
Replying to @ManishEarth @fugueish
I agree that "having null" is an "it's 2017" moment. I don't think "having runtime index errors" is.
2 replies 0 retweets 0 likes -
Replying to @ManishEarth @fugueish
These days I’m kind of skeptical that array index OOB errors would even go away with a sufficiently smart type system.
1 reply 0 retweets 1 like -
True index OOB situations often arise from untrusted input and so have to be dynamic checks anyway.
1 reply 0 retweets 2 likes -
Otherwise, investing in better iterator APIs strikes me as a better use of time than proof systems. Far better usability for similar results
1 reply 0 retweets 3 likes -
Agreed for sequential access, not so sure for random access. Can e.g. sorting be implemented safely w/out dynamic checks or static proofs?
2 replies 0 retweets 0 likes
Yeah, sorting’s an example of something where eliminating the checks basically forces you to prove the algo is correct (I think).
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.