Programming with Proofs - Computerphile
Вставка
- Опубліковано 2 вер 2021
- Continuing our look at the Agda programming language, Professor Thorsten Altenkirch shows us how you can work with proofs, which could be invaluable in some industrial situations.
/ computerphile
/ computer_phile
This video was filmed and edited by Sean Riley.
Computer Science at the University of Nottingham: bit.ly/nottscomputer
Computerphile is a sister project to Brady Haran's Numberphile. More at www.bradyharan.com
I love Professor Altenkirch so much
The way he formats his Python code hurts my PEP-8 neatfreakery though...
Software engineers: Can't wait to write software that's PROVEN to be safe!
Also software engineers: Just had to hack this thing together in about 5 minutes. Hopefully this won't break production XD
Product owner: That's too long, we need this done in a few seconds.
@@P4INKillers Hyper product owner: That's too long, we need this done in a few nanoseconds. Not gonna tell you what you need to do, just that we need it done.
I see you've worked on this task for more than a minute, *_what can I do to help?_*
HR: We have been told you think in "minutes"
That is why we started running unit tests instead of proofs. Tony Hoare, one of the greatest computer scientists who invented quicksort and developed Hoare logic for verifying program correctness and was a great proponent and researcher of formal methods sad this:
"Ten years ago, researchers into formal methods (and I was the most mistaken among them) predicted that the programming world would embrace with gratitude every assistance promised by formalisation to solve the problems of reliability that arise when programs get large and more safety-critical. Programs have now got very large and very critical - well beyond the scale which can be comfortably tackled by formal methods. There have been many problems and failures, but these have nearly always been attributable to inadequate analysis of requirements or inadequate management control. It has turned out that the world just does not suffer significantly from the kind of problem that our research was originally intended to solve."
As much as I love the videos by Prof. Altenkirch and I really tried to follow the previous video, I find it very hard to follow both videos about Agda. So much stuff is going on, when he's typing: Stuff is replaced by placeholders, expanded by some kind of template, what is this "xs", what even is "as", what is cons (is it the "::"?) and how does it behave in Agda, etc... I have to say, I feel kind of lost.... I'd love a more in depth explanation of what the Professor is actually describing in Adga and more explanation of this style of programming...
The professor is performing list manipulation. He's working with a list of numbers (1, 2 , 3) and showing the different ways he can order that list. Reversing it (3, 2, 1), double reverse (which results in the original list), and proving why it works using Agda functional programming language. If you're not used to mathematical proofs via a functional programming language, it can be a bit heavy.
The double colon in this Agda language looks like is used for lists. I've worked with Haskell which looks similar to Agda, and if i had to guess (someone please correct me if I'm wrong), the double colon is used to separate the first element from a list from the rest. So, if you a had list with 1,2,3.... it would be stored as 1 :: 2,3. The first element 1 is the "head" of the list 2 and 3 are the "Tail." Think of lists like a snake, visually, they have a "head" and then essentially their body is a "tail." Probably not anatomically correct but you get the idea...
using variables like x and xs also is an easy way to visually show heads and tails on lists. x would be the list "head" and xs would be the "tail" or the rest of the list.
To have a better understanding of what the Professor is doing, it helps to already know the basics of the language (or just have experience in functional programming) but typically you're only using a functional programming language like Agda/Haskell if you're a really curious person or if you're studying computer science (like i am now). Random fact but Haskell was used to create the Facebook spam filter. Not sure if that's still the case now. So, languages like these do get used in real life! =)
You could have a look at my introductory videos on type theory.
As someone who taught functional programming and formal method verification myself, I will say I myself understood what he was saying, but I definitely felt that a "newcommer" in the field would be completely lost. In the professor's defense though, he tried to convey a LOT of information in just a couple of 20 minute videos.
@@ThorstenAltenkirch Thanks for the reply! I will do that gladly!
As a nearly 20 year developer that's familiar with Haskell and already had some formal proof concepts, this was mostly unintelligible when it started actually talking about proving things. Like, I got the idea of the proof and what the library functions *were*, but what agda is actually doing to turn one into the other was nearly completely opaque.
There seem to be some competition between Altenkirch and Brailsford when it comes to exotic shirts. By the way Altenkirch, I want my shirt back.
This is actually a concept that has not yet gone mainstream but could be suuuper useful! Kudos!
I've been studying this stuff for a while. These videos are incredible useful to me. Thank you very much! ❤️
mathematicians naming functions / parameters:
- use as few letters as possible
- use clever tricks like reverting the order of the letters
- for extra goodness, name all of them the same!
Just kidding, I did exactly the same by naming variables 'aux', 'bux', 'cux' and so on xD
Actually the first rule is use the most outlandish greek letter you can find.
That's why math guys makes the worst developers. Every minute you spend writing clever unique code is 10 minutes wasted for the poor guy who eventually have to update/maintain your code. Also that poor guy might be you a couple of years down the line.
Programmers are responssible for those names though, not mathematicians. Cons and snoc are standard names in functional programming languages. It happens in a lot of cases where something was developed by a handful of people (as opposed to a big company). An example that comes to mind is: if you look at microsift windows API function names, they look like CreateFileEx or CreateProcessA, whereas the linux equivalents are open and fork.
you are ready for programming in assembler, then
@@wertrager assembler is fine if you're working on arduino or simpler stuff. People who write assembly code for x86 chips are madmen.
absolutely love this guy and this topic, more please!
i love how his (snail mail) inbox and outbox are clear.
Loved this video, thanks for showing this off! I think I may actually try my hand at the exercise left for the reader for once
an algorithm that does nothing will pass the test
Because an algorithm that does nothing also satisfies the property being proved. `revrev` isn't proving that `rev` reverses a list, it's proving that `rev` as a function is an Involution (or 'self-inverse'). A "nothing" algorithm is an involution, so it passes the test.
Rewrite it. If the function isn't implemented it should fail.
The goal is not to prove that `rev` is `rev`, but only to prove that `rev (rev x) = x`. The fact that there exist other functions `f` for which `f (f x) = x` is irrelevant to this.
The terms _induction_ and _recursion_ are similar to _morning star_ and _evening star_ which both are the same thing, the planet Venus, but differ in how they're perceived. If I'm not mistaken, one _defines_ things by recursion, and _proves_ things by induction; I've heard _defined by induction_ or, especially in a type theory context, _inductively defined,_ but _proof by recursion_ sounds really off.
Proof by recursion only sounds off until you work in a language like agda for a while 😅
Otherwise you’re absolutely right though: in this context induction and recursion are very closely related if not identical concepts.
"Proof by recursion" is more CompSci-friendly though.
Perhaps a better statement would be “proof by terminating recursion” or “proof by structural recursion”, either of which lines up more precisely with some variety of induction.
Or even better, proof by well founded recursion. And then you hit precisely with well founded induction.
Yes induction and recursion both have base cases induction is mathematical and recursion is computer science.
Great video guys. I hope that you will talk about sel4 in detail.
awesome video I really like these videos on proofs and type theory
I'd love to hear about Prof Altenkirch's Emacs configuration!
2 questions for possible future videos(?). Can one create an FSM using type-theory and how would that go versus set-theory.
2nd. Could you guys talk about modeling control systems like an elevator and converting that model into a state space description, and what would that look if one tried to implement it in a physical system?
Yes, you can formalize Finite State Machines and I have in the past supervised an undergraduate project where the student developed most of the material of our class on Finite State Machines in Coq (also based on Type Theory) including the equivalence of regular expressions on Finite Automata. The nice thing is that you can actually run your constructions which isn't possible in set theory.
I'm not a mathematician or computer scientist, but have an interest in type theory.
To my I would justify the proving of "trivial" properties by calling them building blocks for compound systems, whether they are concerning concurrency, state or anything that is "difficult" in large systems or protocols.
I don't know why I'm surprised that math and CS are related so much
Yeah it is like another world as well when you get into computational theory. Set theory becomes the programming language lol
Can’t have computers without math now… 🤗
Some might argue that CS is simply applied mathematics.
@@nukeeverything1802 I’m surprised who wouldn’t think the two subjects go in tandem with each other.
CompSci is basically the 4th branch of mathematics
I smelled recursion from the beginning and I'm actually starting to think that's recursion is the perfect tool for proving something because it doesn't require you to add new definitions or tools it's a "closed form"
I love how he throws a „na ja“ in occasionally
So amazing I wish I can learn this I'm interested in programming
Reminds me of Coq!
A lot of script assumptions here, can you do this in bash?
I understand the need for proof & i agree fully. But for industrial applications, you would have to prove Agda implementation is free of errors first. And it will be hard as usually recursion is not allowed (there's a good explanation about this in the NASA/JPL "The Power of Ten" paper)
Which tool will make you able to prove whether the adga implementation is free of errors? And then, which tool will prove that the first tool you used is free of errors?
I don't think NASA and others would mind using recursion in proofs about their stuff. Proofs are not executed ever, they're only type-checked. What's bad about recursion is possibly infinite run-time and stack overflow. The infinite run-time is an issue with any language that has a _while_ loop. Tail recursion does not suffer from stack overflow, so not every kind of recursion is bad.
@@Bolpat If it’s never executed on a real target, then it’s safe I guess. I must be too low level to understand this type stuff. I watched all the videos and I still don’t get it
@@jticklemaker1265 You can basically reason about programs in other languages like c inside theorem provers like Agda/Coq if you have some computational model for that programming language. I believe this is what Coq + Verified Software Toolchain does.
Yes, you have an infinite-regression problem: What about the operating system? What about the hardware? The more you verify, the less likely you have bugs. Probably never ever will a system be able to guarantee no bugs.
With CompCert, there's a formally verified C compiler (for the C99 standard, to be precise). So if a compiler (a transpiler to be precise) from Agda to C99 can be verified, you'd have a pretty reasonable basis, something we could expect in the near future. A verified operating system, however, is rather a far-future expectation. Verified hardware is partially a thing of today, but for design/conception only. Hardware not only has to be conceived, but also built, and there's no way to formally verify a building process is bug-free in its execution.
So, we want a program that certifies that another program does its job…
And how did we certify that the certifier does its job?
@Guy Dude Except you aren't trusting the laws of logic. The programmer had to write the routine that checks the other routine, and in the same language. So it's just another programming task, just as susceptible to programmer error.
Good
Couldn't such proofs be used in a compiler substitution optimization.
They are used all the time! I think some optimization passes in LLVM will do this and can eliminate entire loops sometimes
Yes. The GHC compiler allows 'rewrite rules', like 'every time you see 'rev (rev x)', replace it with 'x''. GHC blindly trusts those rules, so it's useful to prove them (e.g. using Agda) to make sure our optimisations don't change the meaning of any edge-cases.
When you talk about lists are you talking about linked lists?
I associate list to be in basic form a linked list
I think he's just talking about a List, and doesn't speficy if it's a linked list. It doesn't really matter as long as the list offers the functions he needs (adding things to list, accessing items in the list, etc). Whatever type of list is up to the programming language implementation. In another language, like Java or C++, he might have to choose a specific type of list (Linked List, Vector, Array List, etc)
This language seems to provide a default 'List' type, which may be implemented as a Linked List, or just as an Array List. But its not a concern of the programmer here
A list in this sense is an abstract data type. It's a structure of some data along with some operations that are irrespective of the implementation details.
@@rosshoyt2030ah, I've never heard of Agda elsewhere. Don't know it. Like all the exercises in basic course of computation are nothing like this but this is an application of that stuff that could be experimented with?
He was talking about it being a cons list, which is a synonym for linked lists
Can you point free the type of revrev somehow?
You mean by saying rev o rev = id? Using functional extensionality this is equivalent to what I have proven. However funext isn't provable in the agda setup I have been using in the video (it has to be postulated as an axiom) but it is provable when switching to cubical which is better in a number of ways (but none of them mattered for this video).
@@ThorstenAltenkirch Yeah, along these lines. But now coming back to the video, it doesn't look as verbose as I first felt it was. Anyways, thanks, it is cool to know that it can be done.
What worth is it to prove something is according to spec when the spec is nonsense...
This follows alot of category theory principles. More or less the same and all polymorphisms in bitween
Isnt this what Cardano are touting but using Haskell?
AFAIK Cardano is written in Haskell because it more directly correlates with the papers than writing it in Java would. (No one writes research papers, and chooses to describe thing with Java)
Haskell is a lot more “production-ready” than Agda. You will have a bad time implementing a server in agda (the ecosystem isn’t there)
@@ilyakooo0 i was under the impression that Cardanos main selling point is that the implementation is somehow formally verified and everything done on the basis of academic approval
AFAIK the company developing cardano is starting to use Agda as well. One of my former students is working for them on this.
We need more math symbols to be standard on qwerty keyboards
The funny thing is it would be incredibly easy to do as well. We already have Fn keys to access separate layers on laptops and compressed keyboards in general, we can do the exact same thing for standard-sized keyboards across even more keys.
Imagine every letter key having a tertiary or even quaternary key-set of symbols behind them. Color-coded, obviously. (the Playstation 3 controllers keyboard had a nice idea using this, it had 2 color-coded modifier keys to access different key-set layers)
Plenty of space to house them visually, without it being an eye-strain. Most keys currently have a binary setup, if you ignore control key signals via modifiers. So small letters + capital letters, numbers + symbols, etc. Some keys require a 3rd via right alt / alt gr, such as the € symbol, or æ. It'd be very easy to make another key for a 4th layer and extend right alt to every key. Heck, you could re-use the apps key / context key button as a 4th layer when it is held down. I use it regularly for hotkeys and symbols because right-click overwhelmingly made that key useless in modern computing.
Agda’s syntax is so beautiful.
WISH I COULD SAY THE SAME ABOUT YOUR MOM
Seeing programs like this one, convinces me that maths is discovered and not fabricated. It's objective, harmonic and real.
Yes and no. Most maths is really more discovered than fabricated (more commonly called invented), but there's exceptions to it.
@@Bolpat Famously set theory, which has multiple contradictory formulations.
Actually if programs and proofs are the same wouldn’t that mean that programs are discovered too? So for example the Linux operating system was discovered? :-)
this is just like when we first did mathematical operands at school. we had to use operands * and after the solution / it back to the core to PROOF that it's a true value.
hehe you can proof that it's unreliable
You should make a video about digital liquid democracy, what a game changer it can be. Flowback is an example of an open source forum with this.
Next step, I'd rather write just the proof, AKA write just the requirements, and have the system automatically generate the program to satisfy it.
You certainly want more automatisation wether full automatisation is even desirable is another question. When you write a program in your head you reason why it works, maybe you try to explain your reasoning in comments but using a system like agda with more automatisation you basically explain your reasoning to the system which then fills in the gaps to create a proof (= program).
i don't have any clew of what's going on
Basically, what's happening is that you specify a bunch of types to the compiler, the compiler does some reasoning, and points out you haven't covered all your cases, but rather than having to compile and run everything, you get immediate feedback rather than getting a core dump or some weird behaviour, so you have to deal with it rather than shrugging and ignoring the issue.
So these are the unit tests of the agda language.
Wow, all that for double reversing a list? This would be just about impossible to use for actual work.
a) this is a toy example
b) It is not about reversing the list, but the property that rev is the inverse function of itself. AND after you prove it there is no input that will not satisfy that property.
@@quirinertz4780 Regarding A, that's kind of the point. It's a toy example and already pretty complex. How does this scale to real-life applications?
@@DominusTerrae This example fits a really common pattern, where 'f (g x) = x' (i.e. f is the inverse of g). In this case 'rev' is its own inverse, so 'rev (rev x) = x'. More real-life examples would be things like 'parse (render x) = x', 'load (save x) = x', etc. Other common patterns are "idempotency", e.g. 'sort (sort x) = sort x', 'cleanup (cleanup x) = cleanup x', etc. "commutativity", e.g. 'f x y = f y x', "associativity" e.g. 'f x (f y z) = f (f x y) z', etc.
"Wow, all that just to turn a switch on/off? These transistors would be just about impossible to use for actual work"
If you need to definitely proof that your code won't break, you have to invest a buttload of time. There is no easy way out.
I don't understand how "rev (rev x) == x" proves more, than just "x == x". It just seems extra steps for tautology. What is the justification or basis for the epistemology?
It is supposed to prove something about the function rev itself, namely that rev is self inverse. It seems tautological because rev is already suggestively named (EDIT: Or rather because it is really trivial but that is because it's supposed to be an easy example).
If rev x were “x appended to x”, then rev(rev x) would not be x.
So, rev(rev x) = x isn’t a tautology.
Ok, thanks. I was way too tired when I watched the video.
He talks about having a program that would take another program as input and automatically prove that program correct (if it is correct). How does that not run afoul of the Halting Problem?
The automatic prover is allowed to give up and run forever.
@@meithecatte8492 It is provable if a program halts after n steps. The automatic theorem prover does something similar. It can prove a subset of all theorems and there are certainly things that it can't prove, but it is allowed to say so after some time. That does not mean it is unprovable only that the theorem prover can't find the answer.
Since all programs in Agda terminate the Halting problem doesn’t play a role here. But maybe you mean Goedels incompleteness? Indeed there are properties you can’t prove or disprove but the one I proved obviously isn’t one of them.
@@meithecatte8492 If there are some programs where it gives up and runs forever, then the "Prover" isn't really a universal proving program. I don't mean in the practical sense -- it could still be very useful for many programs, but I understood from the professor's comment he meant a mathematically "perfect" Prover that can take _any_ arbitrary program and either prove it's correct, or tell you it's incorrect, but not go into an infinite loop.
@@ThorstenAltenkirch "all programs in Agda terminate" How can we be sure of this?
Aren't unit tests in a sense programs that prove properties about other programs?
Yes, but unit tests can only prove "existentially quantified statements", i.e. "there exists an input for which this property holds" (that input is whichever value we're using in our test). Dependent types like Agda let us prove "universally quantified statements", i.e. "this property holds for all possible inputs".
If your input set is finite, you can theoretically have tests that have 100% coverage, thus proving a property for all inputs. But generally unit tests don't prove anything
👍👍👍💻
Couldn't understand
Giesl lässt grüßen
You could just write rev as
Rev (a::as) = rev as :: [a]
Removing the need of an auxiliary function
Nope, because you can only append on the left. Appending a list to a list doesn't make sense, that's why you need concatenation.
Id rather deal with runtime exceptions than write code like this.
Man this is giving me ptsd about programming by contract using fcking Eiffel.....
With the exception fo the syntax being even worse ;D
422th
422 _ND_
@@androidrandom9979 I was going to say that, but you did it 1th
One order of magnitude off of perfection.
You can’t understand recursion until you understand recursion
when in a foreach loop with php how do i mererge all eliments using current eliment number - end of array and have that as last eliment?
interestingly, you seem to have reached the worst possible video within which to ask a PHP question. the language and programming paradigm being discussed here is like the complete antithesis of everything that PHP is known for. why are you even here?
@@computer-love I'm not sure being harsh makes you seem smarter than the person asking the question.
@@josephgaviota im not sure why you even posted at all, just wanted to grandstand? virtue signal a bit?
hes on the wrong website to ask these questions, literally everyone here knows about stackexchange
@@samb443 So, being mean is the right solution?
It's OK to disagree without being disagreeable.
@@josephgaviota i've been told that i unintentionally come off as harsh at times, but here i'm honestly just perplexed
What an accent
I'm surprised Deepmind hasn't worked on this yet. Well, maybe they have but didn't get spectacular enough results to publish anything (and if so it would be sad because a negative result would still be a result).
So, he wrote a unit test?
A proof tells you that a property holds for all possible inputs, while a unit test only shows that a property holds for a subset of all possible values.
No, because with unit tests, you're making a bunch of statements about how you expect something to work and they may be true or not, but here, the _compiler_ is continually saying "show me what you got!", and nuking your home planet if you get the function definition wrong. There's no room for error.
(Well, it just tells you that your proof is incomplete, but close enough.)
@@lukejoshua Not only that, but you can have bugs in your unit tests introduced by the test writer that lead to false passes, whereas the only way the proof term is incorrect is if the type checker has an error.
@@MadocComadrin well, your proof can also be a proof of the wrong thing.
Like, if I name a function ProofOfRiemannHypothesis but the definition is just that of revrev, presumably I’ve made a mistake.
@@MadocComadrin "whereas the only way the proof term is incorrect is if the type checker has an error."
If I write the proof then I can make a mistake in it, fullstop.
Middle
You can put your head to my tail!
OwO
UwU
oWo
Not to sound like a propaganda-infused guy, but I think an interview with Kevin Buzzard (who is also working on a programming language dedicated to mathematical proofs, which is LEAN) would be just as interesting