Possibly naive question from someone who's never worked with this kind of language, but something I've been wondering about:
> it is possible to prove mathematically that your code behaves in precise accordance with its specification
So that bridges from one thing to another; but what prevents flaws in the specification itself? Is it just simpler/easier to read than the code is, so they're easier to spot?
> Is it just simpler/easier to read than the code is, so they're easier to spot?
Kind of. You basically annotate your program with pre/post-conditions, then you run the program through a theorem prover, which attempts to prove all of your conditions are true in all cases.
The basic guarantee is that if you pass the theorem prover, your code will be free of array out-of-bounds accesses, null pointer dereferences, integer overflow, divide by zero, and other runtime errors. These are useful security properties to prove always hold, and you don’t have to explicitly write specifications for them (just conditions to help the prover along).
If you want to go further (prove functional correctness of your program), you can add more specifications. A lot of times you just want to prove some basic sanity checks hold 100% of the time (e.g. always return a sorted array). These can be pretty easy to specify correctly.
> it is possible to prove mathematically that your code behaves in precise accordance with its specification
So that bridges from one thing to another; but what prevents flaws in the specification itself? Is it just simpler/easier to read than the code is, so they're easier to spot?