Conversation

anyway it's a lot of work and, while it would benefit the world, we think we can do more to help the world in the political domain rather than by spending our time building things.

Irenes (many)

@ireneista

thank you for asking.

crow emoji

@glaebhoerl

sounds like something

might be interested in :)

Oh neat! I'm currently making a dependently typed data description language at

@yeslogic

- the intension is to describe existing binary data formats, but that is a big challenge, hehe. Trying to chip away at it. I really like the sound of this!

Using it as a basis for other tooling sounds really cool. :) :)

> we got bogged down in the type checker. haaaa! The struggle! I'm implementing it directly in Rust, but it often feels cumbersome and slow. I do wonder if I would have been better served making more prototypes.

Irenes (many)

@ireneista

yeah the challenge is basically that most of the people who understand dependent type checkers are mathematicians rather than programmers. so all the explanations of it are, um, abstract.

Rob Rix‎

@rob_rix

and there’s so tragically little holistic discussion of how e.g. unification fits into a bidirectional typechecker, and why you might want it to, and how much of a pain in the ass the lang can be to use without it, and how nightmarish a thing it is to self-teach