Haskell for Imperative Programmers #41 - Formal Verification (using Isabelle)

[@romanuslureaus2176]

This Haskell series is a godsend: clear and concise. Question: Do you write a script for each video, or is everything improvised?

[@philipphagenlocher]

Thank you! Most of my videos are improvised. Videos that are very definition heavy (like the videos on category theory, algebra, proofs) are scripted because I don't want to get anything wrong. Longer videos (like this one) that are just showcasing something would take ages to script ;) Ofcourse I'm thinking of what I want to say beforehand and also have some cuts in the recording but otherwise it's just me rambling!

[@romanuslureaus2176]

@@philipphagenlocher I'm honestly surprised because everything you say comes so clear and precise. I started learning some Haskell for a university course and your Haskell videos have been a great supplementary material. Thanks :-) Btw you should consider uploading your videos to Odysee (odysee.com/). Would love to see you there. Anyway... keep the great job you're doing!

[@TheRedbeardster]

Thank you very much! A lot of specifiec features here remind me some features in Lean4.

[@callanmcgill]

Really huge fan of seeing this in your overview and the general effort you put into these videos both in terms of production and of the content included. I wonder how you came across Isabelle? Did you use it in university/ are you a graduate student or did you just learn about it for fun?

[@yecinemegdiche3202]

I'm in the same university as Phillip, and it's taught and maintained by the chair of logic and computation at the department of informatics at the TUM. So yeah, there's a big chance TUM students who are interested in functional programming will find their way to Isabelle, since there's a course about "Functional Data Structures" that uses Isabelle/HOL to formalize and implement purely functional structures

[@philipphagenlocher]

Thanks so much for the kind words! Yecines reply pretty much summed it up! I came across Isabelle in the aforementioned "Functional Data Structures" lecture. Since most of my studies are revolving around software verification this topic was near and dear to my heart! :P

[@gabrielmachado5708]

I began your series last week. I'm still at lesson 15 but I swear I will get here hahah.

[@philipphagenlocher]

Slow and steady ;)

[@Fanaro]

@@philipphagenlocher Nope, put it on 2x and hope for the best.

[@gungunpanda8135]

Thank for your effort!

[@FelipeBalbi]

This is such a great overview of proof assistants in general, thank you for producing this. One small question though: at around 1:11:50, where you define sortedT_values_set, isn’t it redundant to have both lv and rv test for equality too? I mean, wouldn’t it be enough to have lv v? Or do you really need both subtrees to include equality test too?

[@philipphagenlocher]

Thanks so much! The definition of sortedT_values_set HAS to include the equality, otherwise our statement is incorrect. Isabelle can check that with the "nitpick" command: l = Leaf r = Node Leaf a1 Leaf t = Node Leaf a1 (Node Leaf a1 Leaf) v = a1 Here we have a possible counterexample if we only check for "rv > v". The problem is, that we make no assumption about HOW the tree was built in the sortedT_values_set lemma (we never specified that insert is the only function allowed to insert values into the tree). Another counterexample would be any balanced tree that only contains one unique value one hundred times. The inorder traversel would still be considered sorted, thus the tree would be considered sorted. TL;DR: We need the equality because our lemma assumes the tree to be sorted. Sortedness (the way we defined it) allows for this equality on the right subtree.

[@FelipeBalbi]

@@philipphagenlocher Thanks for the extra information :-)

[@mlliarm]

Amazing video. I'm interested bin formal verification of computer programs. I know that for programs written in strongly typed languages this is something pretty mainstream. Do you know what happens with dynamic typed languages? I've found a related PhD, but I was hoping for something more perhaps. Keep up the good work!

[@gourabghosh5574]

Okay I have seen first 6-7 videos of this playlist as haskell is in our syllabus. I want to know how haskell is useful? Why should we learn haskell instead of python, java, etc? Is this only for some fun and challenge to solve every problem by recursion or it can also do something important which other languages can't do?

[@philipphagenlocher]

The answer depends on what you want to do with a programming language. Haskell is not as popular in the industry as languages such as C, C++, Python, Java, etc. So if you want to learn a programming language in order to apply it in an industrial context, Haskell should not be your first choice. However, Haskell is unique in MANY ways. It is one of the few "purely" functional programming languages and is the only language (as far as I know) that uses lazy evaluation efficiently as its default evaluation strategy. Thus, Haskell is fundamentally different from other languages and forces you to think differently about how you structure programs and how you think about program correctness. That's why Haskell is primarily used for teaching and research. So if you are interested in the theory of programming and functional programming in particular, learning Haskell can "open your eyes" on many different concepts in a way that no other language could. Personally I also feel that Haskell allows for cleaner definitions of data structures and algorithms which leads to fewer bugs and overall nicer code... But that's just personal preference ;)

[@enderger5308]

Hi, First off, this series is great. It finally helped Monads click for me and is quite enjoyable. Anyway, I would love to see a few topics covered: 1. Cabal (specifically, the non-project variant) 2. Finding usable libraries in Hackage.

[@miguelmattos4356]

Thank you a lot for the classes! Extremely good :D Is there any way to import haskell code to Isabelle?

[@philipphagenlocher]

Thank you! As far as I know there is no automatic way of converting Haskell to Isabelle HOL but I might be mistaken. :P

[@halbgefressen9768]

However, there is an Isabelle/Haskell module which you may want to have a look at.

[@Fanaro]

But how exactly does Isabelle do all this? Are there limitations? How the hell can a program prove anything from type theory? (I don't actually know if it uses type theory, that's just a guess)

[@philipphagenlocher]

Isabelle uses a wide selection of different methods. I'm no expert when it comes to the internals but what I do know is that Isabelle uses logical resolution and tableaux proving for it's standard prove-procedure. Additionally, sledgehammer invokes SMT- and resolution-based provers for brute-forcing. Isabelle is capable of proving our programs because of the large background theories it contains. At it's core it only understands basic logic. All the other concepts have been formalized in Isabelle itself, thus they are considered proven and can be used for logical resolution. There are MANY limitations. Without our input, Isabelle is absolutely incapable of proving almost any program. We can tell Isabelle to do an induction proof but (as far as I know) there is no reliable way of doing that automatically. The proof is still the users job, Isabelle just fills in the details and checks wether our steps are correct! Still, it is a monumental task and sometimes I am surprised myself what Isabelle and other programs like it can do. :)

[@brydust]

Hi. I've worked on Isabelle for about a year now... have you got any resources for verification of imperative programs via Isabelle ?