Is Coq really the closest thing out there to a stable (i.e. not a research platform) dependently-typed language?
Conversation
Replying to
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.
Replying to
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
Show replies