Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at app.getonboardai.com. Learn more →
Similar projects and alternatives to introit
ChatGPT with full context of any GitHub repo. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at app.getonboardai.com.
introit reviews and mentions
Yatima: A programming language for the decentralized web
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
Sure, thanks for the feedback. Our standard library is here: https://github.com/yatima-inc/introit, I'll edit the README to make that more prominent
As far as docs and tutorials, we weren't planning on doing a public release for another month or two, so there isn't anything yet. The language is still pre-alpha, so our focus has been on getting the core working correctly before smoothing the on-ramp.
Also, tbh, I'm not 100% settled on what the user-facing syntax should be. Right now we have a simple lisp-like core syntax, but I'm thinking about implementing something like Racket's #lang declaration to allow the user to define and import frontends to that core syntax.
Their explanation is reductive, but it looks like more than that. For example, in the standard library  the definition of the Map type is a function of other types.
A note from our sponsor - Onboard AI
app.getonboardai.com | 22 Feb 2024
lurk-lab/introit is an open source project licensed under MIT License which is an OSI approved license.
The primary programming language of introit is Nix.