4 ms·

I started my PhD recently, and in the process I've had to learn Isabelle/HOL, and I gotta say that using it sort of feels like you're unlocking the keys to unde

I started my PhD recently, and in the process I've had to learn Isabelle/HOL, and I gotta say that using it sort of feels like you're unlocking the keys to understanding the universe. Like, I understand that it's fundamentally still code, and so there are potential bugs in the kernel, but shear versatility and level of automation you get within Isabelle/HOL makes the development and understanding of proof feel like outright magic sometimes. Proof is really hard, and having a powerful tool to mechanically check it has nearly limitless potential.

auggierose 4y ago
Amen!
thomasdziedzic 4y ago
> using it sort of feels like you're unlocking the keys to understanding the universe. Completely agree! > having a powerful tool to mechanically check it has nearly limitless potential As someone working in the industry and playing with theorem provers in my spare time, I've never been able to bridge the gap between industry and theory enough to be able to use these formal methods on projects that I'm on.
- tombert 4y ago
  Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. My PhD is in regards to proving properties about robotics, so maybe in 5-6 years I'll have fully bridged industry and theory, but I wouldn't hold my breath :) [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
  - DennisP 4y ago
    Theorem-proving gets some use in the Ethereum community. Smart contracts are an ideal application for it: the code is short and bugs can be disastrous.
  - JadeNB 4y ago
    > Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. As someone who doesn't code for a living, I am certain that this is a naïve question, but, if you want to use theorem-proving software for verification of existing code, does that require employer permission? Is the issue something like, e.g., you need the theorem-proving software and the code to be verified on the same machine, and you're not allowed to install the theorem-proving software on a work machine or to move the code to a non-work machine?
    - tombert 4y ago
      I meant that I couldn't get budget to do it. Obviously I could do a code verification in my free time, but my goal was to start the project with everything that could be written in FStar being written in FStar, with my coworkers onboard. I had root access to my laptop so I could install anything I wanted, but it's hard to do anything if you don't have budget allocated to do so. EDIT: I also should point out that I wanted to export the code from FStar to F# and use the exported and verified code.
    - bluGill 4y ago
      I work on a project that is 20 million lines of code - while large someone reading this is working on a project much larger. There is no way any human working alone can prove the whole thing. I have no idea how to even get started. Even if I did, until I can prove theorem proving is useful in the real world I'm stuck doing it as a side project: my boss will encourage it, but if I spend no more than a couple hours a week one it Now in my company we are worried about bugs and reliability. If I can show via example that theorem proving catches bugs they will train all developers on it and demand all code be proved. However proving quality needs to be something that is worth the effort, if it slightly increases quality but at the expense of making projects take 10 times as long it is probably not worth it except for specific areas of concern.
      - tombert 4y ago
        I feel like it's much harder to shoehorn in proofs to existing codebases than it is to start with the proofs first. The automation in Isabelle is quite good; good enough to where I don't feel that writing pure new code with proofs takes me a prohibitively long amount of time (about 2-3x writing the equivalent Haskell) (sledgehammer ftw), but I can't imagine trying to retroactively go and prove any of my old projects that are considerably smaller than 20 million lines. One big perk for using Isabelle (or other proof systems), outside of the obvious correctness proofs, is being able to prove equivalence. If you can inductively show that two functions have the same inputs and outputs (say one was quick to write or easy to prove things about, the other is efficient), then you can tell the code exporter to replace any instances of the inefficient version with the efficient version. This means that your optimization is proven safe, and is done for free, which is worth its weight in gold when used correctly. Of course, this really only applies to pure and mathey functions. It's substantially harder to prove properties about business logic.
joshmarlow 4y ago
Off topic, but I'm an engineer whose math extends (shakily) into basic proofs (though I'm rusty). I tinkered quite a bit with Lean a couple of years ago and felt comfortable with it as a language, but I don't actually grok how to use it effectively for proving theorems (I'd love to get into formal verification). Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?
- opnitro 4y ago
  Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.
- tombert 4y ago
  Software Foundations (mentioned in a sister comment) is great, and highly recommended. If you want something more Isabelle-focused, the Concrete Semantics book is pretty good [1]. Not exactly the same, but if you want something a bit more approachable than Isabelle or Coq or Agda, it might be worth looking into TLA+. That can introduce you to predicate logic and state machines and set theory if you're not already familiar with them, and TLA+ is a lot more programmer-centric and less pure-mathey than Isabelle. TLA+ offers model checking for "brute force" verification, and also offers a formal proof system called TLAPS. Lamport's talks on TLA+ are quite good [2], and I found that learning Isabelle was a lot easier once I had a lot of practice with TLA+. [1] http://concrete-semantics.org/ http://concrete-semantics.org/ [2] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html

auggierose 4y ago

Amen!

thomasdziedzic 4y ago

> using it sort of feels like you're unlocking the keys to understanding the universe. Completely agree! > having a powerful tool to mechanically check it has nearly limitless potential As someone working in the industry and playing with theorem provers in my spare time, I've never been able to bridge the gap between industry and theory enough to be able to use these formal methods on projects that I'm on.

tombert 4y ago
Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. My PhD is in regards to proving properties about robotics, so maybe in 5-6 years I'll have fully bridged industry and theory, but I wouldn't hold my breath :) [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
- DennisP 4y ago
  Theorem-proving gets some use in the Ethereum community. Smart contracts are an ideal application for it: the code is short and bugs can be disastrous.
- JadeNB 4y ago
  > Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. As someone who doesn't code for a living, I am certain that this is a naïve question, but, if you want to use theorem-proving software for verification of existing code, does that require employer permission? Is the issue something like, e.g., you need the theorem-proving software and the code to be verified on the same machine, and you're not allowed to install the theorem-proving software on a work machine or to move the code to a non-work machine?
  - tombert 4y ago
    I meant that I couldn't get budget to do it. Obviously I could do a code verification in my free time, but my goal was to start the project with everything that could be written in FStar being written in FStar, with my coworkers onboard. I had root access to my laptop so I could install anything I wanted, but it's hard to do anything if you don't have budget allocated to do so. EDIT: I also should point out that I wanted to export the code from FStar to F# and use the exported and verified code.
  - bluGill 4y ago
    I work on a project that is 20 million lines of code - while large someone reading this is working on a project much larger. There is no way any human working alone can prove the whole thing. I have no idea how to even get started. Even if I did, until I can prove theorem proving is useful in the real world I'm stuck doing it as a side project: my boss will encourage it, but if I spend no more than a couple hours a week one it Now in my company we are worried about bugs and reliability. If I can show via example that theorem proving catches bugs they will train all developers on it and demand all code be proved. However proving quality needs to be something that is worth the effort, if it slightly increases quality but at the expense of making projects take 10 times as long it is probably not worth it except for specific areas of concern.
    - tombert 4y ago
      I feel like it's much harder to shoehorn in proofs to existing codebases than it is to start with the proofs first. The automation in Isabelle is quite good; good enough to where I don't feel that writing pure new code with proofs takes me a prohibitively long amount of time (about 2-3x writing the equivalent Haskell) (sledgehammer ftw), but I can't imagine trying to retroactively go and prove any of my old projects that are considerably smaller than 20 million lines. One big perk for using Isabelle (or other proof systems), outside of the obvious correctness proofs, is being able to prove equivalence. If you can inductively show that two functions have the same inputs and outputs (say one was quick to write or easy to prove things about, the other is efficient), then you can tell the code exporter to replace any instances of the inefficient version with the efficient version. This means that your optimization is proven safe, and is done for free, which is worth its weight in gold when used correctly. Of course, this really only applies to pure and mathey functions. It's substantially harder to prove properties about business logic.

joshmarlow 4y ago

Off topic, but I'm an engineer whose math extends (shakily) into basic proofs (though I'm rusty). I tinkered quite a bit with Lean a couple of years ago and felt comfortable with it as a language, but I don't actually grok how to use it effectively for proving theorems (I'd love to get into formal verification). Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?

opnitro 4y ago
Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.
tombert 4y ago
Software Foundations (mentioned in a sister comment) is great, and highly recommended. If you want something more Isabelle-focused, the Concrete Semantics book is pretty good [1]. Not exactly the same, but if you want something a bit more approachable than Isabelle or Coq or Agda, it might be worth looking into TLA+. That can introduce you to predicate logic and state machines and set theory if you're not already familiar with them, and TLA+ is a lot more programmer-centric and less pure-mathey than Isabelle. TLA+ offers model checking for "brute force" verification, and also offers a formal proof system called TLAPS. Lamport's talks on TLA+ are quite good [2], and I found that learning Isabelle was a lot easier once I had a lot of practice with TLA+. [1] http://concrete-semantics.org/ http://concrete-semantics.org/ [2] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html