I suppose, in a sense, it's true - Idris 2 the language combines lots of things that exist already. I don't want to invent any new features. The goal, now, is to make fancy type level programming (which we know is capable of so much good stuff) more widely accessible.
-
-
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
got a link to the thread?
-
I'm not giving it publicity... I'm sure you can find it!
- 1 more reply
New conversation -
-
-
Never mind the trolls. There are always a few bad apples in every community, especially on /r/programming. Idris 1 was an eye-opening experience for programmers with no background in Dependent Types, and Idris 2 looks even better! :-)
-
I don't mind, and so really I shouldn't draw attention to it... It's a very narrow view of what counts as "research" though.
- 3 more replies
New conversation -
-
-
"Done" and "executed into a usable language" are drastically different notions, and IMO conflating one for the other is the most armchair critique you can make of any language effort. In theory, there is no different between theory and practice. In practice, however...
-
As far as I could tell, this person thought "someone knows how to do it" and "everyone already does it" were equivalent. I'm certainly not going to stop having fun because Someone Is Wrong On The Internet :)
End of conversation
New conversation -
-
-
That situation seems to have worked well for Rust: I mean, they knocked out that language design, implementation, infrastructure, documentation, and community in…oh some number of minutes.
-
And managed to verify its soundness and implementation in.... oh wait

- 1 more reply
New conversation -
-
-
I can't wait to see what HN says.
-
This Tweet is unavailable.
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.