When we have such a rich proof term language like Gallina, the tactic language is just one of many possible interfaces. We could just as well build alternative front-ends for proofs for users from different domains or different levels of expertise. Why don't we do that more?
Conversation
Idris 2 is built in a way that makes this possible: the AST for desugared, pre-typing code is exposed as a library, so you can write your own frontends.
It would be cool to see this in Coq. I'd love a more Agda-like frontend for Gallina/Equations.
1
1
14
can we just give up on Gallina and just have Talia's future work apply to Idris 2. I mean mean no offense, and I'm not informed very well on this, but my impression is that Idris2's design is just a lot cleaner than Coq's (whole package, the Coq kernel seems decent).
3
6
It is so Haskelly :(
2
2
I also think the type system is more complicated
2
2
so this is where you would know better than I, but my impression was that cubical type theory was a very nice system that solves lots of the gross problems with things like setoids in Coq, albeit you're paying for this in having to learn a bit more up-front, maybe..?
3
1
I like cubical, I think Idris 2 uses linear types though?
4
4
Yeah, Idris 2 is specifically non-cubical, e.g. there's type-case, so you can refute univalence.
There have been rumblings of getting extensionality by adding OTT to Idris 2 on slack, but I don't think anyone has committed to it yet.
3
4
Ohhhh is type case bad for univalence? Is there a place I can read up about this or is it a folklore thing?
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Oh cool!
…unless this actually meant as a joke? Sorry I'm not great at the subtle theory stuff 😅
2