The other thing we give up, I suppose, is pretending. We can’t get away with treating nontermination effects as if they weren’t there. Hence eval : Term -> Delay Value which we can write for any Turing-complete Term. Business only as usual, made explicit.
-
Show this thread
-
When we put that "Delay" in the type, or write a fuel-driven approximant, we're often accused of somehow cheating, but we're only telling the truth: we can't show this is finite but we can run it as long as you want. That's the *only* deal for partial languages.
1 reply 2 retweets 17 likesShow this thread -
Hilariously, we're also accused of "giving something up" by not allowing arbitrary symbolic execution of infinitary programs at *compile* time. The truth is that we can safely do a hell of a lot more compile time execution of programs than in partial languages.
2 replies 1 retweet 15 likesShow this thread -
That's to say, yes, we're giving something up, compared to GOD. We're giving nothing up, compared to YOU.
1 reply 4 retweets 21 likesShow this thread -
Many people start out correctly pointing out that total languages are subject, as are partial languages, to fundamental limitations on computability. Yes. They then invent and disseminate negative consequences which are total fiction.
2 replies 2 retweets 4 likesShow this thread -
And yes, we're all schmucks in the face of the future. I'd like to enforce "done in three microseconds", not just "done eventually". We're only at the beginning of the honesty journey.
4 replies 8 retweets 29 likesShow this thread -
There are legitimate concerns about the pragmatics of totality. Inevitably, to get more promises out, you have to put more evidence in. Today's overly syntactic termination oracles leave a lot of room for improvement. But talk of programs we "can't write" is bunk.
1 reply 5 retweets 23 likesShow this thread -
-
Replying to @trannosaurusma @pigworker
It’s like...they thought there can be no reduction on coinductive terms?
1 reply 0 retweets 3 likes -
Maybe they ran out of fuel at just the wrong time
-
-
Replying to @edwinbrady @trannosaurusma
Ah, but defaulting to a bogus output is even worse!
0 replies 0 retweets 2 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.