Hi HN, I made this with the idea that many people are somewhat familiar with TypeScript and first-order logic, so combining them could be a nice introduction to automated theorem proving. My CS freshman logic class woefully lacked an interactive code environment<p>It's completely web-based so you can go ahead and try the interactive tutorial <a href="https://peanoscript.mjgrzymek.com/tutorial" rel="nofollow">https://peanoscript.mjgrzymek.com/tutorial</a> . Everything is explained on its own terms, so it should be readable if you just know programming.<p>If you already know this kind of stuff and want a tldr, there is also a reference <a href="https://peanoscript.mjgrzymek.com/reference" rel="nofollow">https://peanoscript.mjgrzymek.com/reference</a> and playground <a href="https://peanoscript.mjgrzymek.com/playground" rel="nofollow">https://peanoscript.mjgrzymek.com/playground</a><p>The code is out on GitHub <a href="https://github.com/mjgrzymek/PeanoScript" rel="nofollow">https://github.com/mjgrzymek/PeanoScript</a><p>Have fun!
You can also see my post on reddit where I answer some questions <a href="https://www.reddit.com/r/ProgrammingLanguages/comments/1jfxjn3/i_made_peanoscript_a_typescriptlike_theorem_prover/" rel="nofollow">https://www.reddit.com/r/ProgrammingLanguages/comments/1jfxj...</a>