4 ms·

> a decent programmer still has a better idea of whether something is correct than the proof system used here. The proof is correct in the language it's writte

> a decent programmer still has a better idea of whether something is correct than the proof system used here. The proof is correct in the language it's written for, Lean. If you change the context (axioms) of a proof then the proof may be invalidated. This is not a surprising thing to anyone who spends a second thinking about it.

Joker_vD 1y ago
> anyone who spends a second thinking about it. Except most programmers don't spend even a second to think about it, and we end up with "int mid = (low + high) / 2;" bugs in standard implementations of binary search in e.g. Java. And that implementation even had a written proof accompanying it!
- Jtsummers 1y ago
  Try that in SPARK/Ada. It'll stop you there [if it can't prove that low + high won't overflow]. Don't take a proof written with one set of assumptions (in this case how integers are expected to behave) and translate it to another language where those assumptions don't hold.
  - zelphirkalt 1y ago
    Are writing our next program in Lean then? Where does that run? There seems to be a fundamental difficulty here. Either we prove things in the language we want to use, which means modelling the behavior of the things we use in that language, or we prove things in Lean, but then cannot apply that to an actual implementation, because of issues like the one above. I would be surprised, if there was no standard approach for modelling bounded integers and their specific properties in a language (which can differ) in a proof language like this. There must have been more people having thought about this and come up with solutions.
    - bollu 1y ago
      yes, Lean is executable, and the proof of natural numbers runs with arbitrary width integers. they're stored as tagged pointers, with upto 63bit numbers being normal numbers, and larger numbers become GMP encoded.
    - Jtsummers 1y ago
      > Are writing our next program in Lean then? Where does that run? That first question is hard to parse. If you mean "Are you writing your next program in Lean then?" then: No, but in principle we could, it runs on each OS we use (Windows and Linux, standard x64 hardware). If you mean something else, I can't figure out what it would be. > Either we prove things in the language we want to use Sure, I mentioned SPARK/Ada. There are systems for C, Java, and others that also work and understand their types so you don't have to add extra modeling. > which means modelling the behavior of the things we use in that language It would already be done for you, you wouldn't have to model Ada's integers in SPARK, for instance. > we prove things in Lean, but then cannot apply that to an actual implementation, because of issues like the one above. https://lean-lang.org/doc/reference/latest/Basic-Types/Fixed-Precision-Integers/#fixed-ints https://lean-lang.org/doc/reference/latest/Basic-Types/Fixed... If you knew your target system was using fixed-width integers, you'd use this.
      - MobiusHorizons 1y ago
        What hardware doesn’t use fixed width integers?
        Jtsummers 1y ago
        What's the context of your question? Did I say otherwise? Some languages (what's being discussed here) give you arbitrary precision integers, like Lean. So the proof in the blog applies to Lean and any issues with things like -INT_MIN not existing isn't a factor in the proof. That's what's being discussed. The proof for C or Ada or something else with fixed-width integers will be different (and the algorithm, likely) to account for that difference and any other relevant differences.
  - touisteur 1y ago
    The most interesting part of SPARK for me is how all the runtime checks are implicitly, automatically generated and need to be proved. A whole bunch of assumptions about the language are hidden and the verification conditions are generated automatically for the underlying automatic or semi-automatic proof tools (why3-intermediated) - the second best part of SPARK. You have to trust that the SPARK FrontEnd makers got it right - or you can inspect/review all the discharged VC if you want - and you still have to actually prove or help prove them all, but I'm not losing sleep over a forgotten 'normal' check.
- lmm 1y ago
  > Except most programmers don't spend even a second to think about it, and we end up with "int mid = (low + high) / 2;" bugs in standard implementations of binary search in e.g. Java. And that implementation even had a written proof accompanying it! I see this as far more of an indictment of Java than an indictment of programmers. If you make the symbol "+" part of your programming language's syntax (especially in a language where you don't allow custom implementations of "+") then it should do what the ordinary mathematical + operation does!
  - cjfd 1y ago
    Do you realize that making + do what the ordinary mathematical + does, is quite expensive? It requires arbitrary precision arithmetic and hence, potentially, memory allocations.
    - lmm 1y ago
      > Do you realize that making + do what the ordinary mathematical + does, is quite expensive? It requires arbitrary precision arithmetic and hence, potentially, memory allocations. Yes I do. It's an acceptable cost in most cases (you will note much of the world runs on Python, a language in which + does behave sensibly, these days), and dangerous optimisations should be opt-in rather than opt-out. In the worst case you should at least make your language fail-stop definite by making it error when the result of + is too large rather than silently continuing in an invalid state.
      - Tainnor 1y ago
        > In the worst case you should at least make your language fail-stop definite by making it error when the result of + is too large rather than silently continuing in an invalid state. That's what Swift does fwiw. But there are downsides to that too (although they're also related to Swift not having a good fault recovery mechanism). In practice, whenever you know you're going to use large enough numbers in Java, you probably want to use BigInteger or BigDecimal (e.g. in banking). Unfortunately, Java doesn't allow you to use the + operator with it.

Joker_vD 1y ago

> anyone who spends a second thinking about it. Except most programmers don't spend even a second to think about it, and we end up with "int mid = (low + high) / 2;" bugs in standard implementations of binary search in e.g. Java. And that implementation even had a written proof accompanying it!

Jtsummers 1y ago
Try that in SPARK/Ada. It'll stop you there [if it can't prove that low + high won't overflow]. Don't take a proof written with one set of assumptions (in this case how integers are expected to behave) and translate it to another language where those assumptions don't hold.
- zelphirkalt 1y ago
  Are writing our next program in Lean then? Where does that run? There seems to be a fundamental difficulty here. Either we prove things in the language we want to use, which means modelling the behavior of the things we use in that language, or we prove things in Lean, but then cannot apply that to an actual implementation, because of issues like the one above. I would be surprised, if there was no standard approach for modelling bounded integers and their specific properties in a language (which can differ) in a proof language like this. There must have been more people having thought about this and come up with solutions.
  - bollu 1y ago
    yes, Lean is executable, and the proof of natural numbers runs with arbitrary width integers. they're stored as tagged pointers, with upto 63bit numbers being normal numbers, and larger numbers become GMP encoded.
  - Jtsummers 1y ago
    > Are writing our next program in Lean then? Where does that run? That first question is hard to parse. If you mean "Are you writing your next program in Lean then?" then: No, but in principle we could, it runs on each OS we use (Windows and Linux, standard x64 hardware). If you mean something else, I can't figure out what it would be. > Either we prove things in the language we want to use Sure, I mentioned SPARK/Ada. There are systems for C, Java, and others that also work and understand their types so you don't have to add extra modeling. > which means modelling the behavior of the things we use in that language It would already be done for you, you wouldn't have to model Ada's integers in SPARK, for instance. > we prove things in Lean, but then cannot apply that to an actual implementation, because of issues like the one above. https://lean-lang.org/doc/reference/latest/Basic-Types/Fixed-Precision-Integers/#fixed-ints https://lean-lang.org/doc/reference/latest/Basic-Types/Fixed... If you knew your target system was using fixed-width integers, you'd use this.
    - MobiusHorizons 1y ago
      What hardware doesn’t use fixed width integers?
      - Jtsummers 1y ago
        What's the context of your question? Did I say otherwise? Some languages (what's being discussed here) give you arbitrary precision integers, like Lean. So the proof in the blog applies to Lean and any issues with things like -INT_MIN not existing isn't a factor in the proof. That's what's being discussed. The proof for C or Ada or something else with fixed-width integers will be different (and the algorithm, likely) to account for that difference and any other relevant differences.
- touisteur 1y ago
  The most interesting part of SPARK for me is how all the runtime checks are implicitly, automatically generated and need to be proved. A whole bunch of assumptions about the language are hidden and the verification conditions are generated automatically for the underlying automatic or semi-automatic proof tools (why3-intermediated) - the second best part of SPARK. You have to trust that the SPARK FrontEnd makers got it right - or you can inspect/review all the discharged VC if you want - and you still have to actually prove or help prove them all, but I'm not losing sleep over a forgotten 'normal' check.
lmm 1y ago
> Except most programmers don't spend even a second to think about it, and we end up with "int mid = (low + high) / 2;" bugs in standard implementations of binary search in e.g. Java. And that implementation even had a written proof accompanying it! I see this as far more of an indictment of Java than an indictment of programmers. If you make the symbol "+" part of your programming language's syntax (especially in a language where you don't allow custom implementations of "+") then it should do what the ordinary mathematical + operation does!
- cjfd 1y ago
  Do you realize that making + do what the ordinary mathematical + does, is quite expensive? It requires arbitrary precision arithmetic and hence, potentially, memory allocations.
  - lmm 1y ago
    > Do you realize that making + do what the ordinary mathematical + does, is quite expensive? It requires arbitrary precision arithmetic and hence, potentially, memory allocations. Yes I do. It's an acceptable cost in most cases (you will note much of the world runs on Python, a language in which + does behave sensibly, these days), and dangerous optimisations should be opt-in rather than opt-out. In the worst case you should at least make your language fail-stop definite by making it error when the result of + is too large rather than silently continuing in an invalid state.
    - Tainnor 1y ago
      > In the worst case you should at least make your language fail-stop definite by making it error when the result of + is too large rather than silently continuing in an invalid state. That's what Swift does fwiw. But there are downsides to that too (although they're also related to Swift not having a good fault recovery mechanism). In practice, whenever you know you're going to use large enough numbers in Java, you probably want to use BigInteger or BigDecimal (e.g. in banking). Unfortunately, Java doesn't allow you to use the + operator with it.