hpr-knowledge-base/hpr_transcripts/hpr3057.txt

Episode: 3057
Title: HPR3057: Formal verification with Coq
Source: https://hub.hackerpublicradio.org/ccdn.php?filename=/eps/hpr3057/hpr3057.mp3
Transcribed: 2025-10-24 15:56:13

---

This is HACO Public Radio Episode 3,057 for Tuesday, 21 April 2020.
Today's show is entitled Vomal Verification with Cock.
It is the 40th anniversary show of Tuku Toro 2,
and is about 21 minutes long, and carries a clean flag. The summery is
2-2-2 talks about formally verifying code.
This episode of HPR is brought to you by archive.org.
Support universal access to all knowledge by heading over to archive.org forward slash donate.
Hello and welcome to the HACO Public Radio. I'm Tuku Toro and today's episode is
about Cock. Cock, that's a French for Rusta, is an interactive
theorem for that I have been toying around with it reasonably.
As usual, all the code samples and such will be in the show notes.
If you can, it might be a good idea to follow along there.
So I wanted to do something on some computation about flagpipes,
originally. And this is a simple model that takes
between the elementary school pilot class. So you have a gene that has three
allele and based on those allele, you get a flag type.
So there's a allele of A, B, and O. And respective flag types are A, B,
A, B, and O. So I wanted to model this in Cock.
So I started by defining types in Cock. They are defined as inductive
flag type allele, colon type, colon equals, and then list of the constructors
separated by a byte. So I have a flag type A, flag type B, and flag type O.
And this is the allele, the specific version of the gene.
And each human most of the time, at least, if there hasn't been any mistakes
along the way, have two of these, one inherited from the father and one inherited from the mother.
So then the flag type, I defined as an inductive flag type, colon type, colon equals,
and again, the constructors separated by the pipes. So type A, type B, type A, B,
and type O. This is the resulting plot type. So if you have, for example,
you have plot type A and plot type B allele, the resulting plot type A, B.
So we need a nothing between these two things, of course.
And in Cock, there are at least two ways of defining functions.
There's a simple definition, and then there's the fixed point that is used to define recursive functions.
The recursive functions can be a bit pretty sometimes, because Cock has a requirement
that all the functions have to produce a value. So we don't have exceptions,
and we don't have infinite recursion. So when you are defining a recursive function,
you have to define it in a way that the compiler can figure out that if this actually terminates or not.
But luckily for us, we don't have to worry about that, because our function flag type,
with our logo case, is a simple mapping.
You get two parameters of plot type allele, and paste of the two parameters,
it will have a value of plot type. So it's a simple mapping.
So it's defined as a definition, plot type, pattern, A, B,
colon, plot type allele, cosparin.
It's defined as a two parameters, A and D, and they are of plot type allele.
And then continuous, colon, plot type.
This is the retool value, colon equals, and then comes the actual function definition.
Here we have a match, A, B, with, this is a, well, pattern match, basically.
And then each pattern is separated by the pipe from each other.
So there's a plot type A, plot type A, arrow type A.
This means that when A is plot type A, and D is plot type A,
then this function will have value of pipe A.
And then we have a, each and every combination here.
And Cox compiler will make sure that you cover each and every gauge.
It won't compile code, but that doesn't cover each case because,
like I said, every, every, every function in Cox has to always produce a value.
They have to be total. This, this is because, I think,
I understood that it's because this is a mathematical tool.
So you have to, you have to have a, if you define a function,
you have to have a value for hold domain.
Okay, so now we have a function.
And we, we have two types.
So we can give that function two types.
I do, do values, and it will produce as a value.
We can write it out as in an interactive mode, writing compute,
open burn, plot type, and then say plot type B, plot type A,
close frame, and dot of course.
And when we evaluate that, it will produce as a type AB.
So this is nice.
Not nice and all, but the interesting part about Cox,
like I said earlier, that it is an interactive theorem program,
meaning that you can state theorems and you can prove them,
or at least try to prove them.
So for our, our function, I have a two theorems.
First one is a written as theorem, dot double over results all type.
Color, it is the name of the theorem.
Plot type, plot type O, plot type O equals pipe O.
Because this means that when a plot type function is applied
with plot type O and plot type O parameters,
it will have value of type O.
This is a theorem.
And then prove what that is.
Prove.reslexivity.qed.
This is a so simple theorem that Cox is able to reason.
It all by, all of it by just a reflexivity.
It basically just, it basically simplifies the left and right side of the theorem.
Now this is that they are the same and it's heavy.
And every theorem always ends with q, q, e, d.
That's laughing form a court error,
the ones from to some along the lines.
Basically means this is what was supposed to be proven.
Infinite that's emotee.
Michali dot dot dot.
Okay.
And now, if we had a more complex theorem,
we would be using a plot type function for some reason.
And we would notice that there's a pattern that matches to this theorem.
We could use this theorem
to help solving that more complex theorem.
Okay.
So let's try the another one.
I'll use it more complex one.
This one is called, this is written as a theorem.
Not double O does not result over type, colon.
So if you have a,
if you have something that is not two plot type O's,
you're not going to get the O type as a result.
I mean type O as a result.
And this theorem is stated as for all,
open parent T1, T2, colon, plot type allele,
close parent, comma.
So for every plot type allele,
T1 and T2, the following holds.
The B1 is not equal to plot type O.
O, T2 is not equal to plot type O.
implies plot type D1, T2 is not equal to type O.
So if plot type function is applied to something
that is not plot type O to plot type O values,
it will not produce type O result.
It will produce something else.
This theorem does not say anything about that,
but it states that it won't be type O.
The proof for this one is in the show note.
It's a little bit more longer.
I'm not going to go through it line by line,
because I don't, frankly, I don't understand this theorem,
but the theorem proving bell enough,
so that I could explain it.
But the basic idea is that we are using this struct for B1 and T2,
that is a case study in the theorem proving part.
So we are proving this theorem
by going through a basically applying plot type function
to each and every value and observing what happens.
So first we are going to call it a plot type A and plot type A.
And we are using a discriminated tactic
to look to observe that these two things
apply to plot types are different than type O.
Tactics are sort of a tool used in the theorem proving.
There's a reflexivity.
It's probably the easiest one.
It simplifies to both sides of the theorem
and observes that they are the same.
Discriminate observes that they are different
and the struct makes a case that it goes through all of each and every possible case.
There's a lot and lots of these in the cork.
And I think you can even write your own if the existing ones
for some reason aren't enough.
The third one mentioned in the proof is simple.
That just simplifies without trying to observe
if they are the same or not.
And contradiction is the last one that I used in this theorem.
It basically proves if you end up with contradiction
like true equals to false, you can use the contradiction
to prove that because of this previous thing holds.
In any case.
And again the theorem ends in QED meaning that this has been proven.
So now if we have a case, if we have some theorem somewhere else
that talks about that has a plot type V1, V2.
And we know that the P1 is something else that plot type.
No, you know that the result won't be typo because of this theorem.
If you pay really close attention, you know that notice
that I defined this if then manner.
So if these parameters are not plot type all,
then the plot type V1, V2 is not typo.
I could have defined that if and only if because then the relation
would hold to the both directions.
But I want to try with a little bit simple, simple way.
Because now this theorem can be only used from plot type.
And this can only used in one direction.
If we had to use the if and only if, as I said,
basically the arrow pointing to the both directions,
then we could reason it to the both directions.
It would be a much stronger theorem.
But one step at a time.
And then in the show notes data,
how this would be written in a mathematical notation,
I don't know how to pronounce all these things.
But basically it's the same.
For all P1, P2, P1 is not plot type all,
all P2 is not plot type of,
then plot type V1, P2 is not typo.
That's basically the gist of the thing.
So my light theorem proving.
I of course could have written this function in a half scale,
or any other language, and written a bunch of.
I could have said it was really sternly and reason inside my head
that yes, this works correctly.
Or I could have written a bunch of unit tests.
I could have used even quick check to produce
near random data for testing.
And with this small function, the quick check
most likely will cover all possible cases.
But with using the mathematical theorem
and reasoning and proving it,
we can show that this is exactly how this function works.
There's no question about that now.
Of course, the theorems are only as good as the starting point.
So if I had the specification of this function incorrectly,
then no theorem could make it magically work correctly.
I would only prove that I can only prove that this theorem,
I mean, this function now follows this specification that I was given.
But if that specification is incorrect,
or I misunderstood that then this tool is not going to fix anything.
And the cook on the other hand,
cook will, when I make this theorem and prove it,
the cook will verify it.
It will keep track of that I have covered all the cases
and that my reason is sane.
So this is on the other hand, this is really powerful tool
because now I can give this function these types,
these theorems and proofs to a colleague of mine
and they can be fairly sure that hey,
that's what it is supposed to do.
And they can step through the proof line by line
and observe how the proof evolves
and what cook displays value are proving it.
But now that we have a function in the cook,
what can we do with that?
Glad that you asked because how I came to this tool
is because of the following.
We can add at the bottom of the source line,
if you had defined this in a module called genes.
We can add at the bottom of the source line,
source code, two lines,
extraction language, Haskell, and extraction genes,
the name of the modules.
When we compile the module,
it will compile it normally,
but in addition to that,
it will output Haskell code that I copied in the show notes.
The data type definitions are quite close to what I have written.
And the plot type function has correct signature.
It has the correct behavior.
The code itself is a little bit odd looking.
For me, that's not how I would have written it by hand,
but it does what it is supposed to do.
So now that I had a,
originally I had a specification
that told me how to,
how this function is supposed to work,
I wrote the types and the implementation of function in cook
using the Galina language,
Galina is a French for hand, by the way.
And proved some properties about it.
I proved that if you have
plot type O, plot type O,
as a parameters to the plot type function,
it will produce a type O.
And I also proved that if you have anything else,
it will never prove.
It will never produce type O.
So now we know how the type O,
plot works in this function.
And we could write more proofs about how to,
how different combinations of all LLS work.
And then we, after proving that code,
we extracted it into the Haskell.
And now I can take that Haskell code
and throw it in some program
and say that this piece of code
don't have to be tested,
because it has been mathematical proven to be correct.
Of course, that bit of,
bit of a stretch,
because you have to consider how it fits
into the parameter scheme of things.
And you might have missed,
or might have missed some cases when proving.
Like I said,
the result is only as good
as the initial specifications
and the hotel rooms.
Because if you have incorrect specifications
or misunderstand the specification
and have packed hotel rooms,
then this isn't going to fix your code.
That if you have those correctly,
this will help you to write code
that is correct.
And it's formally verified
to do what it is supposed to do.
I add a couple links into show notes.
There's a book,
or actually four books,
software foundations.
That I have been reading.
It starts from the very basics
and calls all the way to the
about writing formally verified algorithms.
And then there's a book in a hurry.
That's a 50 page short book
that you can read through to have an idea
that you can do with this tool.
That's what I had about this subject
for this time.
The best way to read me
is nowadays via email
or in the fediverse.
There are two tools
that are mastered on the social,
questions, comments,
and so forth.
Welcome to Ad Astra.
You've been listening
to Hecker Public Radio
at HeckerPublicRadio.org.
We are a community podcast network
that releases shows every weekday
Monday through Friday.
Today's show, like all our shows,
was contributed by an HPR listener
like yourself.
If you ever thought of recording a podcast,
then click on our contributing
to find out how easy it really is.
Hecker Public Radio was founded
by the digital dog pound
and the infonomicon computer club
and is part of the binary revolution
at binwave.com.
If you have comments on today's show,
please email the host directly,
leave a comment on the website
or record a follow-up episode yourself.
Unless otherwise status,
today's show is released
under Creative Commons,
Attribution, ShareLive,
3.0 license.