It's infinitely more approachable than Coq/PVS or whatever other theorem prover since it was designed for teaching and not a research tool or potential applicat

It's infinitely more approachable than Coq/PVS or whatever other theorem prover since it was designed for teaching and not a research tool or potential application to actually verifying properties of complex systems.