[MUSIC]
What are some lessons we can take from formal methods?
Well, let's take a look at formal methods a little bit.
I promise you, there'll be minimal math here.
Formal methods for our purposes have three things.
You begin with the specification of what the program is to do.
You then design it and show that your design matches the specifications, or
satisfies the specifications, to use the correct term.
You then do the implementation and
show that your implementation satisfies the design.
By transitivity, that means it satisfies the specifications.
Now, there is more beyond this, deployment and so forth,
where formal methods really become somewhat informal themselves.
So we're not going to focus on them because now we're only focusing on
the program.
Now, specification, how can you do mathematics with code?
Well, first thing is you state your goals
using a very precise language called specification language.
It's either mathematical or logical, and there are many of these languages.
SPECIAL, PVS is the one that's fairly widely used now, as is HOL and so is Z.
There are a number of others as well.
And the first thing you do is express your specifications in these languages,
in one of these languages.
And then verify it's consistent, that parts of the specification don't
contradict one another, and that the specification will meet the desired goals.
This is typically done through statements of goals as theorems, and
statements of assumptions and such as axioms.
And then you try to prove the theorem based on the axioms and
other things that you've got.
So you're using theorem provers, and verifiers, and so forth.
Okay, so what does that have to do with what we want,
since we're talking informal?
Well, it does mean we have to state the goals clearly and unambiguously so
we know what the program is supposed to do.
The mathematical and logical languages force the first., the clarity.
And the proofs and the verifiers will typically uncover most of the ambiguities.
We don't have those luxuries, though, so we're going to have to focus on
stating the goals clearly and making sure that they don't contradict one another.
Also, we need to be complete, we need to state all the goals we know of.
Because if a new goal comes along, it may mess this up, we'll have to go back and
see whether or not we meet that goal.
The other lesson is the assumptions and axioms of formal methods
correspond to the environment, and the user, and the informal methods.
So we need to understand the environment in which the program runs and
we need to know our assumptions.