4 ms·

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

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.
- practal 4y ago
  Formal verification is just very costly and has diminishing returns. Let's take a CAD program. Which aspects of it would you formally verify? If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification. If you are going for the interesting parts, you will be doing math, essentially.
  - ebingdom 4y ago
    > Let's take a CAD program. Which aspects of it would you formally verify? Any large program will contain some smaller components with relatively well-defined behavior. CAD is not my specialty, so I can't really comment on what algorithms are used in that domain. Forgetting about fancy algorithms for a moment, just having a more expressive type system will allow you to express invariants in your code like the fact that array indices are within the relevant bounds, that you never try to pop an empty stack, etc.—everyday programming issues. For a more concrete example, lately I've been using Coq to formally verify critical properties about a certain type of graph-like data structure I'm using in a system I'm building. > If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification. Most engineers are already writing tests and using static types. Yet, we still have buggy programs. And just to be clear, the kind of formal verification we're talking about is based on static typing. It's just a more expressive type system than what most programmers are used to. > If you are going for the interesting parts, you will be doing math, essentially. You are doing some form of math, but not the kind of cutting edge math that mathematicians do—which was my original point. You are not going to run into the kinds of tricky problems that mathematicians run into with theorem proving software, like universes being too small etc. Most data in software engineering is finite and reasoning about it involves little more than arithmetic and induction (which is just out of reach for mainstream type systems, but not for the kind of type systems used in proof assistants).
    - practal 4y ago
      First, theorem proving is NOT the same as an advanced form of static typing. This is a misunderstanding mostly pushed by computer scientists. Instead of propositions as types, I advocate a more practical form of types, based on Abstraction Logic [0, 1]. Second, yes of course, you can carve out components and concentrate on those. If you can find opportunities for this, great! You will still have buggy programs in which you use those components, to copy your argument. Third, data may be finite, but reasoning about it is often done better in an infinitary context. After all, x^2 + x - 3 is also a finite expression, and much easier to understand than most software. So what? You will find a lot of interesting mathematics done with polynomials, some of it cutting-edge. Saying your software doesn't need cutting-edge math is just limiting yourself and your software. Chances are you will be doing some new (=cutting-edge) math if you try to verify new things. And yes, I run into problems with universes all the time actually, because this is relevant for modular formalisations. It's best to just have a single mathematical universe! [0] https://obua.com/publications/philosophy-of-abstraction-logic/2/ https://obua.com/publications/philosophy-of-abstraction-logi... [1] https://obua.com/publications/practical-types/1/ https://obua.com/publications/practical-types/1/
mbrodersen 4y ago
All of those problems can be proven correct today using Coq/HOL/LEAN etc. see CompCert, seL4 etc. The math needed by Computer Scientists to prove correct is very different from what Mathematicians care about. Look at the mathlib project done by mathematicians in LEAN. It is pretty much useless if you want to prove code correct.
- practal 4y ago
  The topic of mathlib might be different, but the methods are the same. That's why you can use Lean for both in the first place!

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.

practal 4y ago
Formal verification is just very costly and has diminishing returns. Let's take a CAD program. Which aspects of it would you formally verify? If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification. If you are going for the interesting parts, you will be doing math, essentially.
- ebingdom 4y ago
  > Let's take a CAD program. Which aspects of it would you formally verify? Any large program will contain some smaller components with relatively well-defined behavior. CAD is not my specialty, so I can't really comment on what algorithms are used in that domain. Forgetting about fancy algorithms for a moment, just having a more expressive type system will allow you to express invariants in your code like the fact that array indices are within the relevant bounds, that you never try to pop an empty stack, etc.—everyday programming issues. For a more concrete example, lately I've been using Coq to formally verify critical properties about a certain type of graph-like data structure I'm using in a system I'm building. > If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification. Most engineers are already writing tests and using static types. Yet, we still have buggy programs. And just to be clear, the kind of formal verification we're talking about is based on static typing. It's just a more expressive type system than what most programmers are used to. > If you are going for the interesting parts, you will be doing math, essentially. You are doing some form of math, but not the kind of cutting edge math that mathematicians do—which was my original point. You are not going to run into the kinds of tricky problems that mathematicians run into with theorem proving software, like universes being too small etc. Most data in software engineering is finite and reasoning about it involves little more than arithmetic and induction (which is just out of reach for mainstream type systems, but not for the kind of type systems used in proof assistants).
  - practal 4y ago
    First, theorem proving is NOT the same as an advanced form of static typing. This is a misunderstanding mostly pushed by computer scientists. Instead of propositions as types, I advocate a more practical form of types, based on Abstraction Logic [0, 1]. Second, yes of course, you can carve out components and concentrate on those. If you can find opportunities for this, great! You will still have buggy programs in which you use those components, to copy your argument. Third, data may be finite, but reasoning about it is often done better in an infinitary context. After all, x^2 + x - 3 is also a finite expression, and much easier to understand than most software. So what? You will find a lot of interesting mathematics done with polynomials, some of it cutting-edge. Saying your software doesn't need cutting-edge math is just limiting yourself and your software. Chances are you will be doing some new (=cutting-edge) math if you try to verify new things. And yes, I run into problems with universes all the time actually, because this is relevant for modular formalisations. It's best to just have a single mathematical universe! [0] https://obua.com/publications/philosophy-of-abstraction-logic/2/ https://obua.com/publications/philosophy-of-abstraction-logi... [1] https://obua.com/publications/practical-types/1/ https://obua.com/publications/practical-types/1/

mbrodersen 4y ago

All of those problems can be proven correct today using Coq/HOL/LEAN etc. see CompCert, seL4 etc. The math needed by Computer Scientists to prove correct is very different from what Mathematicians care about. Look at the mathlib project done by mathematicians in LEAN. It is pretty much useless if you want to prove code correct.

practal 4y ago
The topic of mathlib might be different, but the methods are the same. That's why you can use Lean for both in the first place!