Does anyone have a preferred or at least "thing I'm aware of" intro to theorem provers? I'm looking at Z3, I've heard of Lean and TLA+.
I've also heard about people using this to "prove" APIs.
In the Ada space I'm aware of Spark, and in C I'm aware of farma-c, but I recognize these are different from the rest.
I'm interested in this. How does this work? How can I experiment with this? I'm not a mathematician or even very educated in any field of mathematics.
When you specify something in one of these languages, how do you actually connect that to working code? How have you proven anything in this case?