I would recommend starting with Idris. It has all the power of a typical theorem prover but feels like a cool programming language. It also has a great book to

I would recommend starting with Idris. It has all the power of a typical theorem prover but feels like a cool programming language. It also has a great book to bring you up to speed: “Type Driven Development”. It will blow your mind.