Is Coq really the closest thing out there to a stable (i.e. not a research platform) dependently-typed language?
Conversation
Sadly it still feels quite a bit like a research platform to me from my attempts to use it. Lots of infrastructural/tooling/dependency duct-tape. Really want a high-quality dependently typed language that's designed for programming first.
1
3
I think Coq is reasonably stable *if you're doing math proofs*, but it was never designed for programming
1
Replying to
Even for that it's a pain. Lots of old-school ideas around imports and namespaces that become a pain when programming at a large scale. At the moment I'm not sure whether my effort is better spent working on something new or trying to knock the existing stuff into shape.
Also focusing on tooling (package ecosystem) and IDE integration from the start is kind of important. But yeah, the problems that need to be tackled are still theoretically hard, and the research platforms still have their place.
1
I just feel that in order to be palatable to current programmers there needs to either be more collaboration between industry and academia, or more industry-led efforts to make bring this stuff across into practical use.
1
1
Show replies