[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.