3 ms·

Stage 8 here: you prove your program works before running it.

by pkrumins 17y ago

minutillo 17y ago
No, that's stage 4.
- pkrumins 17y ago
  4+4.
nostrademons 17y ago
Only works if you can be sure about the behavior and specification of all of your inputs and outputs (not to mention the compiler). Part of getting to stage 6 is realizing that this won't often be the case.
- GeneralMaximus 17y ago
  Well, not very difficult if you're using a functional programming language, where pure and impure code is usually separate. Haskell code can be "proved" just like any other mathematical theorem.
  - ekiru 17y ago
    Assuming that the compiler, any libraries you use, the hardware, and the interfaces to that hardware all behave correctly, yes, you can formally verify code.
  - nostrademons 17y ago
    I wasn't thinking primariy of pure vs. impure, but of user vs. computer. You generally cannot formally verify users, and they often want the dumbest, most illogical things. Like asking that null vs. singular vs. plural cases all be separated out, or that you should filter porn out of their results (what's porn to a computer? hell, what's porn to the supreme court?), or that you should render things brokenly if there's no doctype but do it correctly if there is. One of my cubemates at Google is a project manager who used to work at Microsoft. She said that one of the biggest differences between the engineering cultures of the two companies was that engineers at Google are encouraged to make "product" decisions themselves, while Microsoft engineers basically stuck to code. If a spec was unclear on some point at Microsoft - say, what color of blue to use for the border on some dialog box - the engineer would throw it back over the wall to the PMs and wouldn't work on it until they got further clarification. While at Google, the answer was likely to be "Use your judgment, and we'll fix it if it's terribly bad." That implies some amount of knowledge about what users want, and you generally can't prove what users want.
DannoHung 17y ago
You and the other couple of dozen guys writing in Coq

Stage 8 here: you prove your program works before running it.

minutillo 17y ago

No, that's stage 4.

pkrumins 17y ago
4+4.

nostrademons 17y ago

Only works if you can be sure about the behavior and specification of all of your inputs and outputs (not to mention the compiler). Part of getting to stage 6 is realizing that this won't often be the case.

GeneralMaximus 17y ago
Well, not very difficult if you're using a functional programming language, where pure and impure code is usually separate. Haskell code can be "proved" just like any other mathematical theorem.
- ekiru 17y ago
  Assuming that the compiler, any libraries you use, the hardware, and the interfaces to that hardware all behave correctly, yes, you can formally verify code.
- nostrademons 17y ago
  I wasn't thinking primariy of pure vs. impure, but of user vs. computer. You generally cannot formally verify users, and they often want the dumbest, most illogical things. Like asking that null vs. singular vs. plural cases all be separated out, or that you should filter porn out of their results (what's porn to a computer? hell, what's porn to the supreme court?), or that you should render things brokenly if there's no doctype but do it correctly if there is. One of my cubemates at Google is a project manager who used to work at Microsoft. She said that one of the biggest differences between the engineering cultures of the two companies was that engineers at Google are encouraged to make "product" decisions themselves, while Microsoft engineers basically stuck to code. If a spec was unclear on some point at Microsoft - say, what color of blue to use for the border on some dialog box - the engineer would throw it back over the wall to the PMs and wouldn't work on it until they got further clarification. While at Google, the answer was likely to be "Use your judgment, and we'll fix it if it's terribly bad." That implies some amount of knowledge about what users want, and you generally can't prove what users want.

DannoHung 17y ago

You and the other couple of dozen guys writing in Coq