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?
1
1
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 😅
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Show replies