I'll be the one to tell it : it's a bit weird for the README of a programming language to have an esoteric quote, pages of prose, links to five research papers / theory books, a flame war on build system, a political manifesto and grand visions about the future of programming, but not a single line of, ahem, the programming language in question ?<p>(I hope I'm not missing sarcasm.)<p>Or is it to weed out the people who don't know about beta-reductions ? Am I suddenly in blub world for simply wanting a code example ? Or is there already a tutorial and the link just happens to be missing ?
From the readme, I can't exactly tell what this is for, why I should use it, or how I should use it. Instead the readme is an expression of the creator's ideology. Nothing wrong with expressing that, but without anything concrete to look at and help me understand this project, it just sounds like another ideologically motivated project looking for a use-case.
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]:<p>1. Do you have plans to make Yatima a usable theorem prover?<p>2. If so, how will people typically quotient things (e.g. does it have quotient types)?<p>3. How far does the type theory depart from classical mathematics?<p>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?<p>[0]: <a href="https://github.com/yatima-inc/yatima#motivation" rel="nofollow">https://github.com/yatima-inc/yatima#motivation</a><p>[1]: <a href="https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf" rel="nofollow">https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...</a><p>[2]: <a href="https://github.com/yatima-inc/introit/blob/main/Empty.ya" rel="nofollow">https://github.com/yatima-inc/introit/blob/main/Empty.ya</a>
I think this is a really cool idea. I think you are guys are upto something. I think you need more example, probably an online editor or tutorial. May be there is some, I couldn't find it easily.<p>It still feels very experimental is nature and has feel of a side project. Not sure if you guys are pursuing it seriously. If yes, I would recommend you to create more education material. I think it is very radical idea that has a huge learning curve. Also, I would recommending moving the motivation and manifesto to your landing page if any and focus on getting started, setting up your dev environment and how you could run your first application.<p>Cheers!
If you open a link, and it doesn't work, edit the url:<p>text: leftpad incident<p>link: <a href="https://qz.com/646467/how-one-programmer-broke-the-internet-by-deleting-a-tiny-piece-of-code/from" rel="nofollow">https://qz.com/646467/how-one-programmer-broke-the-internet-...</a><p>fixed: <a href="https://qz.com/646467/how-one-programmer-broke-the-internet-by-deleting-a-tiny-piece-of-code/" rel="nofollow">https://qz.com/646467/how-one-programmer-broke-the-internet-...</a>
Could you explain why did you choose to write your own implementation of DAG instead of using something like petgraph?<p>At first glance I get the feeling that it is really nice! Any elaboration on that would be really appreciated.<p>Good luck with this project. For sure you are on to something. Time will tell. Don’t forget to research industry leaders like Ted Nelson :)
> First-class types. This lets you the programmer to tell the compiler what you intend to do in your program. Then, like a helpful robot assistant, the compiler will check to make sure that what you're actually doing matches those expressed intentions.<p>So static typing? Or am I missing something?
The README makes a lot of bold claims for what, as far as I can tell, seems to be vaporware. Does this language have any kind of effect system yet, or can it only evaluate pure expressions?