Oh, I'm glad this got picked up! I posted it on New Years day and wasn't sure if it was going to be!

As a bit of background on myself and my goals/targets with this.

I started my career as an embedded software developer writing uCos-III for an RTOS working on medical devices for Cardinal Health where I primarily worked on enteral feeding pumps. From there, I spent a couple years in fintech, before trying my hand at my first startup where I co-founded a company in the quick commerce space. (Think similar to Doordash Dashmarts). When that fell apart I took a job at Hasura where I wrote GraphQL to SQL transpilers and other neat things for about 18 months. I've worked across a few different domains and the motivation behind writing this language is that I am preparing to teach my 13 year old brother how to code and wanted something I could get low level with him on, without losing him altogether.

This is a dual-purpose language and has a dual-AST, and the things I'm currently working on... having switched gears towards spending a couple days on the Logical side of things are adding an actual prover to the Logical AST. I'm getting ready to add a derivation tree struct and incorporate the ability to use a solver to do things like Modus Ponens, Universal Instantiation, etc. I also want to upgrade the engine to be able to reason about numbers and recursion similar to Lean with inductive types.

This is an early access product, it is free for students, educators, non-profits, orgs with < 25 people, and individuals.

It would make my day if I could get some rigorous HN style discussions, and even the critiques!! The feedback and discussions are invaluable and will help shape the direction of this effort.

What a lovely surprise doing my daily HN check before bed and seeing this post. :)

EDIT: I will read and respond to comments when I get up in the morning, feel free to ask questions! Or make suggestions.