4 ms·

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 proposi

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/

ebingdom 4y ago
> First, theorem proving is NOT the same as an advanced form of static typing. This Hacker News post is about a theorem prover based on dependent types. That's the context for our discussion. > You will still have buggy programs in which you use those components No one is disagreeing with this claim. But eliminating some bugs is better than nothing, even if you don't eliminate all bugs. You and the other commenters repeating this strawman are doing a lot of harm to people trying to socialize their research. > Chances are you will be doing some new (=cutting-edge) math if you try to verify new things. Citation needed. Most software is not doing anything interesting at all from a mathematical perspective, just shuffling data around. But either way the point is moot—Martin-Löf type theory (which is what this "magmide" thing seems to be based on) can do arbitrarily fancy math if needed (which is rarely). I've been verifying bits of software for about 10 years, and I've never needed to invent new math to do it (though I would be happy if I ever did!).
- practal 4y ago
  Well, if you created a new data structure not known before, and proved theorems about it, that's new math. If you copied a well-known data structure, and prove theorems about it, that's not new math. What do you think mathematicians do? They just examine certain things rigorously and with utmost scrutiny. These things are simpler than things appearing in real-life. Software interfaces with real-life, so cutting-edge math is really a subset of what's needed for software. That is obvious to me, but I don't have a citation. You can cite me, if you want to. Finally, dependent types as it is done today in Coq and Lean etc. is not nice enough a logic to attract mathematicians. The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists? Oh, because your problems are simpler, so you don't need a nice logic? Saying that Martin-Löf type theory can do arbitrarily fancy math is both false and right. Just as saying that anything can be programmed in assembler is both false and right. Yeah, with enough focus and discipline you probably can, but who would want to?
  - ebingdom 4y ago
    > The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists? Type theory has many attractive properties over traditional foundations like set theory. See, for example: https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
    - practal 4y ago
      Citing your link: > At this point, however, you may be feeling that type theory sounds very complicated. Lots of different ways to form types, each with their own rules for forming elements? Where is the simplicity and intuitiveness that we expect of a foundational theory? It's just not there, Mike. Type theory is neither simple nor intuitive, and it doesn't make a good foundation. Type theory certainly has advantages, but it gets lost in esoteric texts like Mike's. There are two simple advantages over set theory within first-order logic: general variable binding, and that things are kept separate, for example that a boolean is not a number. Now, how to do general variable binding without static types I show in [0]. How to still keep things separate, in [1]. All without having to divide the mathematical universe into static types.
guerrilla 4y ago
> First, theorem proving is NOT the same as an advanced form of static typing. Yes it very much is in a dependent type theory.
- practal 4y ago
  Yes, and because of that limitation dependent type theory is an inferior logic for theorem proving.
  - guerrilla 4y ago
    That's silly. Whether it's a good or bad metatheory for theorem proving depends entirely on one's goals and preferences. Most mathematicians use a type theory over something else, so it's hard to even take your view seriously. On top of that, you seem very opinionated for someone who was just confused about the topic of this thread. I have no idea why you're waging a holy war over this but maybe take a break.
    - practal 4y ago
      Most mathematicians don't even use formal logic. For sure they don't use type theory! You seem to be the one who is silly/confused here. If you want to lift your confusion, read the [0] link I gave above.
      - deleted 4y ago
        [deleted]
mbrodersen 4y ago
It literally is. Martin Luff Type Theory is the mathematical foundation used by most proof assistants today. The type checker is the prover. If your code type checks then you have proven a theory. I highly recommend learning more about the Curry Howard correspondence and Dependent Types. It might just blow your mind.
- practal 4y ago
  See my other answers. Curry-Howard is interesting, but making it the foundation of theorem proving is a choice (in my opinion, not a very good one), not a necessity, as most Curry-Howard fans seem to think.

ebingdom 4y ago

> First, theorem proving is NOT the same as an advanced form of static typing. This Hacker News post is about a theorem prover based on dependent types. That's the context for our discussion. > You will still have buggy programs in which you use those components No one is disagreeing with this claim. But eliminating some bugs is better than nothing, even if you don't eliminate all bugs. You and the other commenters repeating this strawman are doing a lot of harm to people trying to socialize their research. > Chances are you will be doing some new (=cutting-edge) math if you try to verify new things. Citation needed. Most software is not doing anything interesting at all from a mathematical perspective, just shuffling data around. But either way the point is moot—Martin-Löf type theory (which is what this "magmide" thing seems to be based on) can do arbitrarily fancy math if needed (which is rarely). I've been verifying bits of software for about 10 years, and I've never needed to invent new math to do it (though I would be happy if I ever did!).

practal 4y ago
Well, if you created a new data structure not known before, and proved theorems about it, that's new math. If you copied a well-known data structure, and prove theorems about it, that's not new math. What do you think mathematicians do? They just examine certain things rigorously and with utmost scrutiny. These things are simpler than things appearing in real-life. Software interfaces with real-life, so cutting-edge math is really a subset of what's needed for software. That is obvious to me, but I don't have a citation. You can cite me, if you want to. Finally, dependent types as it is done today in Coq and Lean etc. is not nice enough a logic to attract mathematicians. The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists? Oh, because your problems are simpler, so you don't need a nice logic? Saying that Martin-Löf type theory can do arbitrarily fancy math is both false and right. Just as saying that anything can be programmed in assembler is both false and right. Yeah, with enough focus and discipline you probably can, but who would want to?
- ebingdom 4y ago
  > The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists? Type theory has many attractive properties over traditional foundations like set theory. See, for example: https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
  - practal 4y ago
    Citing your link: > At this point, however, you may be feeling that type theory sounds very complicated. Lots of different ways to form types, each with their own rules for forming elements? Where is the simplicity and intuitiveness that we expect of a foundational theory? It's just not there, Mike. Type theory is neither simple nor intuitive, and it doesn't make a good foundation. Type theory certainly has advantages, but it gets lost in esoteric texts like Mike's. There are two simple advantages over set theory within first-order logic: general variable binding, and that things are kept separate, for example that a boolean is not a number. Now, how to do general variable binding without static types I show in [0]. How to still keep things separate, in [1]. All without having to divide the mathematical universe into static types.

guerrilla 4y ago

> First, theorem proving is NOT the same as an advanced form of static typing. Yes it very much is in a dependent type theory.

practal 4y ago
Yes, and because of that limitation dependent type theory is an inferior logic for theorem proving.
- guerrilla 4y ago
  That's silly. Whether it's a good or bad metatheory for theorem proving depends entirely on one's goals and preferences. Most mathematicians use a type theory over something else, so it's hard to even take your view seriously. On top of that, you seem very opinionated for someone who was just confused about the topic of this thread. I have no idea why you're waging a holy war over this but maybe take a break.
  - practal 4y ago
    Most mathematicians don't even use formal logic. For sure they don't use type theory! You seem to be the one who is silly/confused here. If you want to lift your confusion, read the [0] link I gave above.
    - deleted 4y ago
      [deleted]

mbrodersen 4y ago

It literally is. Martin Luff Type Theory is the mathematical foundation used by most proof assistants today. The type checker is the prover. If your code type checks then you have proven a theory. I highly recommend learning more about the Curry Howard correspondence and Dependent Types. It might just blow your mind.

practal 4y ago
See my other answers. Curry-Howard is interesting, but making it the foundation of theorem proving is a choice (in my opinion, not a very good one), not a necessity, as most Curry-Howard fans seem to think.