Some random questions to the developers regarding the motivation that "math is more fun when you have a computer to take care of the detail-work" [0]:
1. Do you have plans to make Yatima a usable theorem prover?
2. If so, how will people typically quotient things (e.g. does it have quotient types)?
3. How far does the type theory depart from classical mathematics?
4. The paper you've linked [1] suggests that the standard definition of contradiction is "too strong" in its theory, but that appears to be the definition of Empty [2]. What am I missing?
I would dearly love to make Yatima a usable theorem prover, and Lean has been a huge inspiration particularly regarding syntax. But building a usable theorem prover is a huge project, and at minimum will require substantial work on our theory, on type-inference (which is fairly minimal right now) and on advanced features like quotient types or univalence.
On that point, we've done a little exploration on encoding the Path types from Cubical Type Theory as self-types, and I think there's some promising work to be done there. But I know my limits and while I feel very comfortable building a useful programming language that can do a little bit of basic theorem proving, I know that doing a proper job on a real theorem is going to require larger scale resources.
As far as the link from the Self-Types paper, our theory is similar to their System S, but is not the same. Not 100% sure but I think the main relevant difference here is about Leibniz equality, which iirc allows for saying `a == b` when `a` and `b` are of different types. Yatima's Equal type https://github.com/yatima-inc/introit/blob/main/Equal.ya, implements the more standard homogenous/Martin-Löf equality, but this is just a library, not a language builtin.
We really do need to write an actual paper for Yatima's theory though, especially considering that we've combined the self-types from System S with a variation of Quantitative Types a la Idris 2. Writing that paper is likely step 0 of any Yatima as a theorem prover project, until then we should view Yatima as just an unsound functional programming language with some nice type-level features
1. Do you have plans to make Yatima a usable theorem prover?
2. If so, how will people typically quotient things (e.g. does it have quotient types)?
3. How far does the type theory depart from classical mathematics?
4. The paper you've linked [1] suggests that the standard definition of contradiction is "too strong" in its theory, but that appears to be the definition of Empty [2]. What am I missing?
[0]: https://github.com/yatima-inc/yatima#motivation
[1]: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...
[2]: https://github.com/yatima-inc/introit/blob/main/Empty.ya