Conversation

Personally I'm cool with the trade-off, but I've needed to make peace with the fact that there is no type system that will ever really satisfy me now. I'm optimistic that we are iterating towards a better place though. The future is exciting!

Sorry to bring all this up in people's timeline again - I guess I'm just hoping to encourage empathy and build some bridges! I'm not alone in forgetting that we're all trying to solve hard problems, in different ways!

Steven Shaw

@steshaw

No worries! Haven't seen much except for the Rich Hickey's gist about open source—seems somewhat sour but also understandable and possibly a bit of a hissy/hickey fit. I noticed your secret project in another tweet … so the future of programming _is_ dependently typed, isn't it?

11:56 AM · Dec 3, 2018Twitter Web Client

Replying to

@steshaw

I'm pretty sure it is! But it's still a long road ahead. Many problems still need to be solved, and that's even with all the decades of research poured into it. I do think we need to try to get it into practical usage more though - hence my not-so-secret project :3

Replying to

and

Currently I'm working on core foundational stuff, trying to build a core language that can be relatively easily worked on/understood by compiler people (who might not know the type theory)

Thankfully there are more resources than ever out there for people who want to learn how to work on dependently typed language implementations. The dominoes are starting to line up! It's an exciting time.

Replying to

Good luck with it! A lot of programs can be written easily within an ML-style system but would be nice to know you have the power of dependent types when you need it. I find DT pretty tricky in Haskell and haven't really gotten into them there... but in Idris, it's pretty easy.