8 ms·

I am sure we can do better than predicate logic or types, but the code needs to change also. Code should be more abstract and reusable. If possible, it should b

I am sure we can do better than predicate logic or types, but the code needs to change also. Code should be more abstract and reusable. If possible, it should be a subset of the logic. There is no point in verifying the same stuff in JavaScript, Java, Rust, Swift, ... Furthermore, something that looks simple might need a lot of abstraction to become provable. Something might be simple to write down in code, but in order to come up with a notion of correctness for it, and actually prove it, might require something significantly more complicated. Infatuation with Hoare-Logic is part of the problem (that's what the paper you link uses, I think?). Thinking that verifying programs is easier than doing proper math on the computer is a dead end. First get mathematicians to actually like doing proofs with the help of a computer. THEN you might have a chance of tackling more practical applications like program verification without using an insane amount of resources.

guerrilla 4y ago
> First get mathematicians to actually like doing proofs with the help of a computer. Many are using type theoretic and HOL theorem proves already. What threshold do we need to reach? Isn't Lean HoTT? Isn't that pretty much good enough (modulo UI and tooling)? I ask the latter question because that was the original promise of HoTT but I haven't kept up to date on Lean, so I'm asking.
- practal 4y ago
  The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. A nice example is the recent formalisation in Lean of some ideas by Peter Scholze: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... That's great stuff, which shows what can in principle be done with this technology. But why is a team necessary to formalise Scholze's ideas? Note that Scholze himself doesn't touch Lean. In my opinion, the threshold is reached when Scholze himself sits down DURING the development of his ideas to interact with the proof assistant and develop+verify his ideas.
  - ebingdom 4y ago
    > The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.
    - deleted 4y ago
      [deleted]
    - practal 4y ago
      Not if you do software the right way. Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... Furthermore, I don't think cutting-edge math needs a much different approach from cutting-edge software. You need to be able to express your thoughts succinctly, and have the tools to reason about them. It is often said that software verification is different because there is much more to verify, but on a more shallow level. I instead think software is just not done at the right level of abstraction. Software is at the same time more and less than math. More, because in addition to understanding a topic, you also need an implementation, which has additional issues like speed and memory usage, battery life, etc. Less, because if you do a nice implementation, nobody is asking about its correctness, or how well you understood the topic in the first place. For software today, a nice implementation is much more important than a correctness proof.
      - ebingdom 4y ago
        > Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally. The most common bogus argument I hear against formal verification is that it's impractical to come up with a spec or proof for the entire program, so we might as well not even bother with formal verification at all.
        4y ago
- ebingdom 4y ago
  > Isn't Lean HoTT? No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT. But the good news is you don't need HoTT to verify software. Type theory is already quite capable of it, despite what others in this thread would like you to believe.
  - guerrilla 4y ago
    > Type theory is already quite capable of it, despite what others in this thread would like you to believe. I know but mathemeticians wanted HoTT.
- practal 4y ago
  There was a version of Lean that supported HoTT, and I think it helped in making Lean popular. But that support has been dropped in Lean 3, and Lean 4 does not support it either. Lean 4 itself seems to be a radical rewrite, and libraries written for Lean 3 do not work in Lean 4.
User23 4y ago
Verification is largely a fool's errand[1]. The juicy opportunity is tooling that aids in constructing programs such that they necessarily have the desired properties. Predicate transformer semantics are up to the task. It's basically just applied lattice theory, which is a very well understood field of math and within the learning capacity of any competent programmer. Edit: Automated verification does however attract a lot of research money as the latest in a long list of fads promising the bean counters that they can hire cheap idiot programmers instead of expensive smart ones. I don't mean to be dismissive though, the automatic verification research is genuinely interesting and they have accomplished impressive things, for example[1]. [1] https://www.semanticscholar.org/paper/Learning-Loop-Invariants-for-Program-Verification-Si-Dai/b56fcbc32adcbe19caec31aaaf0fe045db5ad2b3 https://www.semanticscholar.org/paper/Learning-Loop-Invarian...
- practal 4y ago
  Automated verification is not the latest in a long list of fads. First, it is not a fad, and second, it has been around for a long time (check for example [0], which dates from 1961). I agree with you that constructing programs such that they necessarily have the desired properties is the way to go. But we will disagree in how to go about that. Predicate transformer semantics is just another name for Hoare-Logic, and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Rather, I would like to see programs as natural outflows / consequences of verified mathematical theories. [0] https://en.wikipedia.org/wiki/DPLL_algorithm https://en.wikipedia.org/wiki/DPLL_algorithm
  - User23 4y ago
    > Predicate transformer semantics is just another name for Hoare-Logic, Sir Tony is certainly highly influential, but Hoare triples are a considerably more basic. Not to understate their importance, having a solid base to build on is essential. > and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Please provide some explanation so that this doesn't read as an absurdity.
    - 4y ago
mbrodersen 4y ago
Mathematicians are using LEAN today to prove learning edge mathematics correct. Google LEAN and mathlib.
- practal 4y ago
  See my reply to you deeper below.

guerrilla 4y ago

> First get mathematicians to actually like doing proofs with the help of a computer. Many are using type theoretic and HOL theorem proves already. What threshold do we need to reach? Isn't Lean HoTT? Isn't that pretty much good enough (modulo UI and tooling)? I ask the latter question because that was the original promise of HoTT but I haven't kept up to date on Lean, so I'm asking.

practal 4y ago
The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. A nice example is the recent formalisation in Lean of some ideas by Peter Scholze: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... That's great stuff, which shows what can in principle be done with this technology. But why is a team necessary to formalise Scholze's ideas? Note that Scholze himself doesn't touch Lean. In my opinion, the threshold is reached when Scholze himself sits down DURING the development of his ideas to interact with the proof assistant and develop+verify his ideas.
- ebingdom 4y ago
  > The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.
  - deleted 4y ago
    [deleted]
  - practal 4y ago
    Not if you do software the right way. Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... Furthermore, I don't think cutting-edge math needs a much different approach from cutting-edge software. You need to be able to express your thoughts succinctly, and have the tools to reason about them. It is often said that software verification is different because there is much more to verify, but on a more shallow level. I instead think software is just not done at the right level of abstraction. Software is at the same time more and less than math. More, because in addition to understanding a topic, you also need an implementation, which has additional issues like speed and memory usage, battery life, etc. Less, because if you do a nice implementation, nobody is asking about its correctness, or how well you understood the topic in the first place. For software today, a nice implementation is much more important than a correctness proof.
    - ebingdom 4y ago
      > Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally. The most common bogus argument I hear against formal verification is that it's impractical to come up with a spec or proof for the entire program, so we might as well not even bother with formal verification at all.
      - 4y ago
ebingdom 4y ago
> Isn't Lean HoTT? No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT. But the good news is you don't need HoTT to verify software. Type theory is already quite capable of it, despite what others in this thread would like you to believe.
- guerrilla 4y ago
  > Type theory is already quite capable of it, despite what others in this thread would like you to believe. I know but mathemeticians wanted HoTT.
practal 4y ago
There was a version of Lean that supported HoTT, and I think it helped in making Lean popular. But that support has been dropped in Lean 3, and Lean 4 does not support it either. Lean 4 itself seems to be a radical rewrite, and libraries written for Lean 3 do not work in Lean 4.

User23 4y ago

Verification is largely a fool's errand[1]. The juicy opportunity is tooling that aids in constructing programs such that they necessarily have the desired properties. Predicate transformer semantics are up to the task. It's basically just applied lattice theory, which is a very well understood field of math and within the learning capacity of any competent programmer. Edit: Automated verification does however attract a lot of research money as the latest in a long list of fads promising the bean counters that they can hire cheap idiot programmers instead of expensive smart ones. I don't mean to be dismissive though, the automatic verification research is genuinely interesting and they have accomplished impressive things, for example[1]. [1] https://www.semanticscholar.org/paper/Learning-Loop-Invariants-for-Program-Verification-Si-Dai/b56fcbc32adcbe19caec31aaaf0fe045db5ad2b3 https://www.semanticscholar.org/paper/Learning-Loop-Invarian...

practal 4y ago
Automated verification is not the latest in a long list of fads. First, it is not a fad, and second, it has been around for a long time (check for example [0], which dates from 1961). I agree with you that constructing programs such that they necessarily have the desired properties is the way to go. But we will disagree in how to go about that. Predicate transformer semantics is just another name for Hoare-Logic, and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Rather, I would like to see programs as natural outflows / consequences of verified mathematical theories. [0] https://en.wikipedia.org/wiki/DPLL_algorithm https://en.wikipedia.org/wiki/DPLL_algorithm
- User23 4y ago
  > Predicate transformer semantics is just another name for Hoare-Logic, Sir Tony is certainly highly influential, but Hoare triples are a considerably more basic. Not to understate their importance, having a solid base to build on is essential. > and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Please provide some explanation so that this doesn't read as an absurdity.
  - 4y ago

mbrodersen 4y ago

Mathematicians are using LEAN today to prove learning edge mathematics correct. Google LEAN and mathlib.

practal 4y ago
See my reply to you deeper below.