Loading ...
Sorry, an error occurred while loading the content.
 

[XP] Re: Success of XP over Formal Methods

Expand Messages
  • christrobridge
    ... formal ... formal ... through ... Probably ;-). I did a quick revision on wikipedia. It s to do with applying mathematical techniques to prove that final
    Message 1 of 11 , May 2, 2007
      --- In extremeprogramming@yahoogroups.com, "Chris Wheeler"
      <christopher.wheeler@...> wrote:
      >
      > ahem, <shuffles feet, embarrassingly looks elsewhere>..Uhm..what are
      formal
      > methods?...in all my years, I've never used anything I ever called
      'formal
      > methods'...Is this the whole 'prove correctness' thing that I slept
      through
      > in university?
      >
      > Chris.

      Probably ;-). I did a quick revision on wikipedia.

      It's to do with applying mathematical techniques to prove that final
      system meets the requirements. This typically entails using languages
      that have their semantics defined formally (mathematically?). If this
      is done then there is some hope of getting answer to questions such as
      whether two different programs are semantically equivalent, or the
      truth of logical statements concerning the program.

      In theory you'd hope most languages have a sound semantic definition,
      but C and C++ actually avoid this deliberately for various reasons (or
      at least defer the decision to particular implementations).

      Chris
    • John Roth
      The big problem with Formal Methods as I see it today is that it s just too expensive to apply except in areas where the additional correctness/reliability
      Message 2 of 11 , May 2, 2007
        The big problem with "Formal Methods" as I see it
        today is that it's just too expensive to apply except
        in areas where the additional correctness/reliability
        is worth the cost.

        I've commented on the relationship between
        formal methods and TDD before, so to repeat:
        assertions could be dropped into the TDD process
        in exactly the same way tests are included now.
        The difficulty is that there is no theorem prover
        which can validate all assertions in a program of
        reasonable size (about 100 kloc) within the TDD
        window for running tests (that is, about 15 seconds)
        for a useful language (e.g. Java). If anyone cares to
        write one, it would take over the development world
        the same way xUnit has taken it over today.

        John Roth


        ----- Original Message -----
        From: "christrobridge" <chris@...>
        To: <extremeprogramming@yahoogroups.com>
        Sent: Wednesday, May 02, 2007 8:26 AM
        Subject: [XP] Re: Success of XP over Formal Methods


        I think this is confused. Perhaps this is related to the fact that
        Formal Methods tend to be used in circumstances where 'the right
        thing' is very important? - eg safety/life critical applications.

        There is no reason why agile techniques can't be applied to formal
        methods, so in a sense your comparing apples and oranges.

        Formal methods (using a 'formal' language) might actually have added
        benefits as you may be able to verify pre/post condition relationships
        for all inputs rather than just spot cases, as happens with unit
        testing. Then again, that might be beyond the proof checker... or
        even just not computable.

        I think there are several reasons why formal methods haven't taken
        off. One is the cost of using them, another is the level of technical
        skill/ability required is greater than for the more popular languages.

        I think the great flaw in the 'Formal Methods' vision is that it
        missed the (agile) point that a large part of the software development
        problems is people not knowing what they want. It also overlooks the
        possibility that people might actually make errors in the specification...

        The lack of consistency (and formality) in the 'real world' may be a
        problem too. It's one thing to validate that your formally generated
        code is correct for a specific target, but the continual change
        occurring to most platforms these days presumably precludes them?

        Chris

        --- In extremeprogramming@yahoogroups.com, "Matt Heusser"
        <matt.heusser@...> wrote:
        >
        > Paolo Bizzarri Asked:
        >
        > >Now, it has been an interesting question (at least for me) why formal
        > >methods have got so little success, whereas XP have got so much more
        > >success. Both fields were practiced by smart people, interested in
        > >producing better code.
        > >
        >
        > Yes, but the formal methods people were trying to do "The Right
        Thing" (TRT)
        > whereas extreme programming takes the track of "Worse Is Better."
      • Steve Freeman
        ... The interesting bit about Worse Is Better is that the authors had the genius or luck (or both) to implement exactly the right abstractions to make Unix
        Message 3 of 11 , May 3, 2007
          On 1 May 2007, at 03:29, Ron Jeffries wrote:
          > Dick Gabriel is a wonderful and brilliant man. His views of the
          > universe are far darker than mine, however.
          >
          > I do not fully agree with what Worse is Better seems to imply,
          > despite that it is historically accurate.
          >
          > Maybe it's just that I don't want to believe.

          The interesting bit about "Worse Is Better" is that the authors had
          the genius or luck (or both) to implement exactly the right
          abstractions to make Unix and C worth the trouble, same with Berners-
          Lee and the Web. There are plenty of systems out there which are just
          "Worse", so that's not a qualification in itself :)

          S.

          Steve Freeman
          M3P Limited.
          http://www.m3p.co.uk

          Winner of the Agile Alliance Gordon Pask award 2006
        Your message has been successfully submitted and would be delivered to recipients shortly.