7 ms·

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

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.
    - 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).
guerrilla 4y ago
> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. No, you didn't answer the question at all. How many is many? How many will be enough for you? It is being used by mathematicians and for some pretty important things.
- practal 4y ago
  Interesting point. Let's say 1% of all mathematicians. That would be many.
User23 4y ago
Most mathematicians are doing work that is, frankly, formally unsound. There's a huge culture of hidden assumptions in most mathematical fields. Not to mention that the syntax is literally unparseable. For example what does this mean? sin(x) + cos(x) Most mathematicians would say it's the sum of the sine of x and the cosine of x. But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). Obviously that kind of ambiguity is unacceptable in a formal procedure syntax like that used by programming languages. That's just a simple example, traditional math is full of this kind of thing.
- guerrilla 4y ago
  > But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). No it doesn't because math lexes greedily (and is also context sensitive anyway.) 'sin' is a symbol just like 'x'. There's no ambiguity in your example.
  - User23 4y ago
    Thank you for illustrating the culture of assumptions I was referring to.
  - hwayne 4y ago
    Pretty much any mathematician, on seeing `xy`, would think it's `x*y`, and not a new symbol called "xy".
    - deleted 4y ago
      [deleted]
- practal 4y ago
  It's a weird example, but you definitely got a point. Of course, an ambiguity like in your example never causes a problem, because this text is parsed by humans, not by machines!

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.
  - 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).

guerrilla 4y ago

> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. No, you didn't answer the question at all. How many is many? How many will be enough for you? It is being used by mathematicians and for some pretty important things.

practal 4y ago
Interesting point. Let's say 1% of all mathematicians. That would be many.

User23 4y ago

Most mathematicians are doing work that is, frankly, formally unsound. There's a huge culture of hidden assumptions in most mathematical fields. Not to mention that the syntax is literally unparseable. For example what does this mean? sin(x) + cos(x) Most mathematicians would say it's the sum of the sine of x and the cosine of x. But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). Obviously that kind of ambiguity is unacceptable in a formal procedure syntax like that used by programming languages. That's just a simple example, traditional math is full of this kind of thing.

guerrilla 4y ago
> But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). No it doesn't because math lexes greedily (and is also context sensitive anyway.) 'sin' is a symbol just like 'x'. There's no ambiguity in your example.
- User23 4y ago
  Thank you for illustrating the culture of assumptions I was referring to.
- hwayne 4y ago
  Pretty much any mathematician, on seeing `xy`, would think it's `x*y`, and not a new symbol called "xy".
  - deleted 4y ago
    [deleted]
practal 4y ago
It's a weird example, but you definitely got a point. Of course, an ambiguity like in your example never causes a problem, because this text is parsed by humans, not by machines!