Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Case for Formal Verification (2013)

permalink.gmane.org

Post reply on HN
Print view View original

11–20 of 113 posts

Re: The Case for Formal Verification (2013)

#11

Post by Pacabel »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

Your description of TDD is a pretty blatant misrepresentation of the actual philosophy and techniques.

Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check.

Sure, extensive formal verification of all software would probably bring some benefit in terms of correctness and perhaps security. But you're not considering the cost involved.

So far, such verification has only proven to be possible in rather limited situations, namely where there are significant resources available, or in academic exercises. Maybe this will change in the future, but in the present it's generally far more cost-effective to use a statically-typed programming language along with some form of automated testing. That gives many of the benefits of more formal methods of verification, but while also avoiding many of the costs, even if the end result doesn't conform to some theoretical idea of "perfection".

Re: The Case for Formal Verification (2013)

#12

Post by tluyben2 »

ramidarigaz wrote: post #3

Relevant: I attended LambdaConf yesterday at CU Boulder, and there was a _great_ intro workshop for Idris, which is in the same domain as Coq. Idris is similar to Haskell (it's actually written in Haskell), but with a dependent type system, a tactic-based theorem prover like Coq has, and a bunch of other fun features.

Idris is really worth checking out if you have any interest in this kind of stuff. I used Coq and now am playing with Idris and F*; the latter two feel good and practical. With an FP background they are easy to pick up.

Re: The Case for Formal Verification (2013)

#13

Post by betterunix »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

The problem with proofs is that you need to know what to prove, and that is hard. Even formalizing something as seemingly simple as sorting is tough for most programmers. If your formalization of whatever you wanted to implement is wrong, then your proof is worthless -- you have only proved that your program does something other than what it was supposed to do.

It's not that TDD is perfect, but it is a pragmatic approach to reducing bugs and it helps a lot in preventing regressions.

Re: The Case for Formal Verification (2013)

#14

Post by ryanobjc »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

While you are correct, I'm not really sure how I feel about you mocking documentation really.

I guess communicating with your coworkers is pretty passe?

Re: The Case for Formal Verification (2013)

#15

Post by daleharvey »

Pacabel wrote: post #11
dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

Your description of TDD is a pretty blatant misrepresentation of the actual philosophy and techniques. Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check. Sure, extensive formal verification of all software would probably br…

Really confused at why this comment is being so harshly downvoted, it seems fairly accurate, possibly downplaying how useful formal verification may be in the future, but the parent is most definitely misrepresenting the practicality and usefulness of TDD

Re: The Case for Formal Verification (2013)

#16

Post by sliverstorm »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

Perhaps because formal verification is hard & very expensive?

For starters, where does an open source project come up with an entire compute farm...

Re: The Case for Formal Verification (2013)

#17

Post by dkarapetyan »

ryanobjc wrote: post #14
dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

While you are correct, I'm not really sure how I feel about you mocking documentation really. I guess communicating with your coworkers is pretty passe?

I am not mocking documentation.

Re: The Case for Formal Verification (2013)

#18

Post by ryanobjc »

noselasd wrote: post #10
dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

One big advantage is regression testing - which is why you don't just test it in a REPL and forget about it.

Totally agree here, manually verifying a chunk of code once, for example early on in the dev lifecycle, then having it exist inside a big system is really the "EE" way of doing things.

But the reality is you gotta dig deep and change stuff, after all how often does an engineer dive in and change how a transistor works (laws of physics be damned!)

I feel like overall software quality has been harmed by the emphasis of mathematical proof of code. The problem is that it's not currently possible (for a variety of reasons, including underspecified languages, math, research and many others) to formally verify, end-to-end, a real world system (eg: Oracle Database, Salesforce.com CRM, etc).

Over promising on software proof, and under delivering has diverted attention away from relatively simple and "boring" practices to increase code quality.

While people in this thread are mocking TDD, the reality is most code I have seen in a production setting is really bad. Unit tests that aren't, test runs that take 4 hours, complete lack of tests, opaque tests that are hard to debug, and hard to fix. A lot of TDD and agile code/clean code says "let's make the code easier to read, have unit, real unit tests, for everything and refactor and get rid of cruft as often". While these are TOOLS and judicious application applies, in a production code scenario there is often no justification, other than ignorance (always fixable!) to disregard good advice!

To summarize the good advice:

- make code easy to read at a glance

- code should be self-documenting (refinement of the above)

- units should be testable independently

- tests should exist at higher levels, such as integration and end-to-end tests

Just like the 10 commandments, you don't have to believe in Agile or XP to agree with these basic things.

Re: The Case for Formal Verification (2013)

#19

Post by ryanobjc »

dkarapetyan wrote: post #17
ryanobjc wrote: post #14

Earlier quoted context omitted.

While you are correct, I'm not really sure how I feel about you mocking documentation really. I guess communicating with your coworkers is pretty passe?

I am not mocking documentation.

"just glorified documentation"

I think it's pretty well understood that calling something "glorified" is making fun of it. Perhaps I guess you meant to mock TDD but it also seems like you are mocking writing documentation.

While it could cut either way I guess, I decided to take a snap judgement (like 99% of your readers) and call you out on it. Sorry.

Re: The Case for Formal Verification (2013)

#20

Post by dkarapetyan »

Pacabel wrote: post #11
dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

Your description of TDD is a pretty blatant misrepresentation of the actual philosophy and techniques. Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check. Sure, extensive formal verification of all software would probably br…

I did not say all software, just key components as it is pretty clearly laid out in the original article. I disagree with the significant resource aspect as well. I recommend Leslie Lamport's recent talk for some very lightweight ways to get started with formal verification: http://channel9.msdn.com/Events/Build/2014/3-642.
Post reply on HN