Proof assistants are like that. Check out Coq or Agda. If you aren't aware of it already, your spirit is calling for the stuff they talk about a lot in the func

Proof assistants are like that. Check out Coq or Agda. If you aren't aware of it already, your spirit is calling for the stuff they talk about a lot in the functional programming community. See https://youtu.be/IOiZatlZtGU https://youtu.be/IOiZatlZtGU for example. Maybe not the best video or intro to the themes though. Wadler also just put out a book about programming language foundations in Agda - https://plfa.github.io/ https://plfa.github.io/. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... being one of the profound ideas here.