Avdi is a great developer who I have learned a lot from, but I think he is exactly wrong here. A thread.https://twitter.com/avdi/status/1114181834353647616 …
-
Show this thread
-
A syntax error is an error, and errors should be raised at runtime. Therefore, syntax errors should be raised at runtime. This follows from Avdi's argument.
2 replies 0 retweets 17 likesShow this thread -
The alternative is to acknowledge that some errors should be raised at runtime and some should be raised at compile-time. Now we're just haggling about which ones.
1 reply 1 retweet 40 likesShow this thread -
So you might ask: why is checking syntax at compile-time good? It's good because a file with a syntax error is not even a program, and there's no sense in trying to run it at all. This exact argument applies to type errors.
3 replies 6 retweets 59 likesShow this thread -
Replying to @ReinH
Not quite. Rice’s theorem implies typecheckers will reject programs that have no runtime errors. Not the case for syntax errors.
1 reply 0 retweets 2 likes -
Replying to @Blaisorblade @ReinH
Viceversa, you *can* eliminate all runtime errors via types (through correctness proofs), but usually the extra benefits are too expensive. What’s the tradeoff?
2 replies 0 retweets 1 like -
Replying to @Blaisorblade
These things are of course true, but my argument is about pragmatics.
3 replies 0 retweets 1 like -
Replying to @ReinH
I’m also biased by having failed for months to write programs with dependent types that are trivial with normal types. Pragmatically, the amount of typing in ML/Haskell is probably a sweet spot, but I’m not sure how much is the extra cost for type-safe meta programming for most.
2 replies 0 retweets 2 likes -
Replying to @Blaisorblade
I am hopeful that with what we learn from
@edwinbrady's Idris, we will be able to build a new programming language that will show us where the sweet spot REALLY is.2 replies 0 retweets 2 likes -
Replying to @ReinH @edwinbrady
More like, this might move the sweet spot. At the very least, Edwin is trying to bootstrap Idris. Which most other systems aren’t remotely trying. (In part, that might be because of technological choices.)
2 replies 0 retweets 1 like
This is mostly because I want to make a thing in Idris and I don't really know how to do anything else. But I'm still having enormous fun having a go.
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.