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
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.
1
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.
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
I feel like something got lost in translation? I was saying that Coq is pretty reasonable if you're a mathematician formalizing math proofs for mathy reasons and then u said even for that case it's not great but now you're talking about programming again?
1
2
Show replies