Use Idris then. This is why multiple languages exist; there are tradeoffs and you have to compromise.
-
-
Agreed for sequential access, not so sure for random access. Can e.g. sorting be implemented safely w/out dynamic checks or static proofs?
-
Yeah, sorting’s an example of something where eliminating the checks basically forces you to prove the algo is correct (I think).
End of conversation
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.