4 ms·

How does one learn and get involved with formal verification outside academia? What sort of mathematical background is required. I always get lost with pure fu

How does one learn and get involved with formal verification outside academia? What sort of mathematical background is required. I always get lost with pure functional languages and the related subjects, even in the introductory material. Though I’ve been able to understand the usefulness of both some functional concepts (through playing with various impure languages like F# or Erlang) and of formal verification (from looking at SPARK with Ada) but all the notation and vocabulary and such of languages like Isabelle’s HOL and Idris confuse me. I even find myself lost among Scala developers.

amautertt 5y ago
I am further along in the journey, I have been learning formal verification/type theory and logic on my own. I think these two are excellent books, SF : Logical Foundations for the basics, SF: Verified Functional Algorithms. Unfortunately there is no royal road in type theory. This subject is incredibly demanding yet satisfying. Software foundations are excellent books to read even if you aren't interested in verification/program proof.
cybernautique 5y ago
My advice: swing wide. If you don't know where to start, then judge a book by its cover and read it until you hit a knowledge gap, then slither down that gap and keep digging for resources until you either get bored or achieve something. I recommend starting with geometric algebra or topology. The aspiring selfstarter has a bevy of great options. Sidney A. Morris' "Topology Without Tears" is fine androgogy, as is the widely-acclaimed undergrad textbook "Intro to Topology: Pure and Applied" by Colin Adams. The biggest thing, in my opinion, is to realize that there are precious few things you need permission to think, mathematically. The fundamental mathematical advantage is abstraction. If you can manage your abstractions and approach the math as nothing more than especially pedantic philosophy- it helps.
- jhanschoo 5y ago
  I'm sorry, how is geometric algebra and basic topology even relevant to formal verification? Your suggestions sound more related to your own interests. The commenter is better served browsing through some introductory formal verification material like Concrete Semantics by one of the same authors as the linked document.
  - namibj 5y ago
    Not sure about geometric algebra, but topology comes up because it studies the abstract formal structure that connects your problem with other (possibly solved) problems. For example, a couple weeks ago I was musing about optimal vertex renumberings so that "the (0/1) adjacency matrix of a non-densely-connected acyclic digraph's transitive closure" scores well according to a domain-specific compressibility metric. Specifically, at column i and row j is a 1 if and only if (using the post-remumbering indices) vertex i was reachable from vertex j in the original input graph. The compression results from only storing start and end indices of contiguous runs of 1s in a row. [Edit2: the score of a specific vertex renumbering is the the number of such runs for the complete matrix. Only uninterrupted runs of 1's count.] It is easy to see that a renumbering that results in a triangular matrix won't be terrible, and simple deepest-branch-first depth-first enumeration of the input DAG's undirected "version" (one just ignores edge direction for this step) is at least fairly good for sub-quadratic in vertex count (assuming an average degree much smaller than the number of vertices). [Edit1: I forgot to point out that this is extremely close to plain run-length-encoding of the matrix in row-major order, except for the fact that RLE cares about a row-crossing run and I don't.] But exhaustive renumbering testing is O(n!) for n vertices. I think topology could help me, but I'd need to know some topology to find me way around the literature.
    - jhanschoo 5y ago
      I think combinatorics might be more relevant here. I'll note that I mentioned basic topology in my reply, because topology does indeed have deep connections with type theory that most formal verification systems are based on, interpreting types / theorems are spaces, terms / programs / proofs are continuous functions within them.[1] But basic undergrad topology typically studies more well-behaved (read: more like the real number line) spaces than this. [1]: https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf
  - cybernautique 5y ago
    Sorry, you're correct, and I should have made it clearer. This is general advice for getting into math, which is what I took the parent to be seeking advice for.
- mbrodersen 5y ago
  This is really bad advise. Geometric Algebra and Topology has nothing to do with proving algorithms correct. Better advise would be to learn Agda and read examples of,proving things in Agda.
DeathArrow 5y ago
When I was a student in University we used Formal language and automata theory to proof that algorithms are correct. But we studied computer science, not math.
cerved 5y ago
Mathematical notation can be a bit odd and often not wholly consistent. Wikipedia has a good page that lists mathematical notation which can be helpful while you're reading a paper. There are also some mathematical concepts you should have a basic understanding of. Functions and sets. This was taught to me in basic algebra. It's actually mostly super straight forward
- nicklaf 5y ago
  Type theory is like this in particular. My background is mostly in classical math, and I was initially thrown off by the amount of symbols with special meaning used in CS papers. An important realization was that most of the definitions behind these symbols (many I think borrowed from logicians) are actually quite straightforward, and the papers are not necessarily conceptually difficult so much as layered in their use of abstraction. I'll mention that Nederpelt and Geuvers' Type Theory and Formal Proof: An Introduction was recommended to me for this topic. I haven't had a chance to study it yet, but I'd say it's worth checking out.
namibj 5y ago
1) For the "how to get started with formal verification outside academia", I'll first get the case of "in/for production" out of the way: a) "use Z3[0] with some binary/source-language-of-choice/LLVM -lifting to handle relatively simple situations that need to": i) guarantee some assert (often, but not always index-out-of-bounds checks, like non-trivial Rust slice indexing) statements are unreachable ii) some bit hacks compute the same thing as the non-hacked implementation b) "use TLA+[1] to verify concurrent stuff with race conditions": i) in lock-free data structures that don't come with a proof that the algorithms do the right thing (in those cases, just verify three implementation truly matches the proven algorithm) ii) in (network, or sufficiently network-like) protocols that aren't 100% exactly transcribed ports of existing proven algorithms or so simple a finite state machine can (and will) be used 2) For doing it more for fun than short-term gains: a) For getting a handle on pure functional program design, I recommend going through the relevant track of HtdP[2] (Prologue until just before "Arithmetic and Arithmetic" -> I -> II -> III -> Intermezzo 2: Quote, Unquote -> V {-> [if you want to write remotely-performant pure functional code, follow up with:] VI}) b) For learning how to exploit a proof assistant for fun and applied computer science, I'll refer to the guidance provided by Isabelle/HOL. Please use the IRC(/Matrix ?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case. [0]: https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [2]: https://htdp.org/2021-5-4/Book/index.html https://htdp.org/2021-5-4/Book/index.html [3]: [edit: apparently it is neither IRC nor Matrix, but rather Zulip:] https://isabelle.zulipchat.com/ https://isabelle.zulipchat.com/
AlexCoventry 5y ago
I really like the book Software Abstractions

amautertt 5y ago

I am further along in the journey, I have been learning formal verification/type theory and logic on my own. I think these two are excellent books, SF : Logical Foundations for the basics, SF: Verified Functional Algorithms. Unfortunately there is no royal road in type theory. This subject is incredibly demanding yet satisfying. Software foundations are excellent books to read even if you aren't interested in verification/program proof.

cybernautique 5y ago

My advice: swing wide. If you don't know where to start, then judge a book by its cover and read it until you hit a knowledge gap, then slither down that gap and keep digging for resources until you either get bored or achieve something. I recommend starting with geometric algebra or topology. The aspiring selfstarter has a bevy of great options. Sidney A. Morris' "Topology Without Tears" is fine androgogy, as is the widely-acclaimed undergrad textbook "Intro to Topology: Pure and Applied" by Colin Adams. The biggest thing, in my opinion, is to realize that there are precious few things you need permission to think, mathematically. The fundamental mathematical advantage is abstraction. If you can manage your abstractions and approach the math as nothing more than especially pedantic philosophy- it helps.

jhanschoo 5y ago
I'm sorry, how is geometric algebra and basic topology even relevant to formal verification? Your suggestions sound more related to your own interests. The commenter is better served browsing through some introductory formal verification material like Concrete Semantics by one of the same authors as the linked document.
- namibj 5y ago
  Not sure about geometric algebra, but topology comes up because it studies the abstract formal structure that connects your problem with other (possibly solved) problems. For example, a couple weeks ago I was musing about optimal vertex renumberings so that "the (0/1) adjacency matrix of a non-densely-connected acyclic digraph's transitive closure" scores well according to a domain-specific compressibility metric. Specifically, at column i and row j is a 1 if and only if (using the post-remumbering indices) vertex i was reachable from vertex j in the original input graph. The compression results from only storing start and end indices of contiguous runs of 1s in a row. [Edit2: the score of a specific vertex renumbering is the the number of such runs for the complete matrix. Only uninterrupted runs of 1's count.] It is easy to see that a renumbering that results in a triangular matrix won't be terrible, and simple deepest-branch-first depth-first enumeration of the input DAG's undirected "version" (one just ignores edge direction for this step) is at least fairly good for sub-quadratic in vertex count (assuming an average degree much smaller than the number of vertices). [Edit1: I forgot to point out that this is extremely close to plain run-length-encoding of the matrix in row-major order, except for the fact that RLE cares about a row-crossing run and I don't.] But exhaustive renumbering testing is O(n!) for n vertices. I think topology could help me, but I'd need to know some topology to find me way around the literature.
  - jhanschoo 5y ago
    I think combinatorics might be more relevant here. I'll note that I mentioned basic topology in my reply, because topology does indeed have deep connections with type theory that most formal verification systems are based on, interpreting types / theorems are spaces, terms / programs / proofs are continuous functions within them.[1] But basic undergrad topology typically studies more well-behaved (read: more like the real number line) spaces than this. [1]: https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf
- cybernautique 5y ago
  Sorry, you're correct, and I should have made it clearer. This is general advice for getting into math, which is what I took the parent to be seeking advice for.
mbrodersen 5y ago
This is really bad advise. Geometric Algebra and Topology has nothing to do with proving algorithms correct. Better advise would be to learn Agda and read examples of,proving things in Agda.

DeathArrow 5y ago

When I was a student in University we used Formal language and automata theory to proof that algorithms are correct. But we studied computer science, not math.

cerved 5y ago

Mathematical notation can be a bit odd and often not wholly consistent. Wikipedia has a good page that lists mathematical notation which can be helpful while you're reading a paper. There are also some mathematical concepts you should have a basic understanding of. Functions and sets. This was taught to me in basic algebra. It's actually mostly super straight forward

nicklaf 5y ago
Type theory is like this in particular. My background is mostly in classical math, and I was initially thrown off by the amount of symbols with special meaning used in CS papers. An important realization was that most of the definitions behind these symbols (many I think borrowed from logicians) are actually quite straightforward, and the papers are not necessarily conceptually difficult so much as layered in their use of abstraction. I'll mention that Nederpelt and Geuvers' Type Theory and Formal Proof: An Introduction was recommended to me for this topic. I haven't had a chance to study it yet, but I'd say it's worth checking out.

namibj 5y ago

1) For the "how to get started with formal verification outside academia", I'll first get the case of "in/for production" out of the way: a) "use Z3[0] with some binary/source-language-of-choice/LLVM -lifting to handle relatively simple situations that need to": i) guarantee some assert (often, but not always index-out-of-bounds checks, like non-trivial Rust slice indexing) statements are unreachable ii) some bit hacks compute the same thing as the non-hacked implementation b) "use TLA+[1] to verify concurrent stuff with race conditions": i) in lock-free data structures that don't come with a proof that the algorithms do the right thing (in those cases, just verify three implementation truly matches the proven algorithm) ii) in (network, or sufficiently network-like) protocols that aren't 100% exactly transcribed ports of existing proven algorithms or so simple a finite state machine can (and will) be used 2) For doing it more for fun than short-term gains: a) For getting a handle on pure functional program design, I recommend going through the relevant track of HtdP[2] (Prologue until just before "Arithmetic and Arithmetic" -> I -> II -> III -> Intermezzo 2: Quote, Unquote -> V {-> [if you want to write remotely-performant pure functional code, follow up with:] VI}) b) For learning how to exploit a proof assistant for fun and applied computer science, I'll refer to the guidance provided by Isabelle/HOL. Please use the IRC(/Matrix ?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case. [0]: https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [2]: https://htdp.org/2021-5-4/Book/index.html https://htdp.org/2021-5-4/Book/index.html [3]: [edit: apparently it is neither IRC nor Matrix, but rather Zulip:] https://isabelle.zulipchat.com/ https://isabelle.zulipchat.com/

AlexCoventry 5y ago

I really like the book Software Abstractions