Proof assistants are too esoteric for me. Coq, Idris, Agda, Lean, way above my pay-grade. Fair play to people that understand them but I can't. It's tough to ad

Proof assistants are too esoteric for me. Coq, Idris, Agda, Lean, way above my pay-grade. Fair play to people that understand them but I can't. It's tough to admit such a thing on a forum like this but there you go. The closest I think I'll need to go along that route is to graft microkanren into a toy language as part of its type system.