Per VognsenI'm curious if people working on proof assistants are bothered by the complexity of elaboration when it comes to end-to-end correctness. The attitude seems to be that elaboration is a free-for-all playground as long as the core logic is consistent and proof terms expressed in the core logic can be independently checked by a small kernel (the de Bruijn criterion).
francesco 🍥@pervognsen "elaboration" means very different things in different dependently typed languages. The Coq tradition is mostly about having tactics to vomit out some script which proves what you want to prove (and I guess this is the "elaboration" you're talking about).
@pervognsen On the other hand the Agda/Epigram tradition is about surfacing elaboration in some way -- i.e. dependent pattern matching. In that context it turns out that most elaboration can be reduced to higher order unification, see https://arxiv.org/pdf/1609.09709 . So that might give you a sense in which elaboration itself can be fit into a single framework, which might or might not satisfy you :).
@pervognsen I'm not really saying that the Coq way is worse than the Agda way btw -- if anything tacticts seem to be winning (although I'm not up to speed with recent developments). But they are radically different approaches to elaboration.