# Where's formal proof of Haskell's claim to...?

## chris glur — 2015-02-11 15:22:34

    be able to avoid the need to tell the machine what to do step-by-step,

    and just provide it with a <description of the problem>, and allow it

    to workout/search for a route to the solution?

    Since we've learned to accept compilers that work-in-the-dark,

    Haskells claim seems promising.

    Is this a theory that can be demonstrated by graduated examples,

    hopefully published somewhere?

    Is it perhaps related to unification - like prolog?

## Michael Haufe — 2015-02-23 18:52:46

    On Wed, Feb 11, 2015 at 9:22 AM, chris glur wrote:
     > Where's formal proof of Haskell's claim to be able to avoid the need to
    > tell the machine what to do step-by-step, and just provide it with a
    > <description of the problem>, and allow it to workout/search for a route
    > to the solution?
     [...]
     > Is this a theory that can be demonstrated by graduated examples,
    > hopefully published somewhere?

     Do you have a specific quote in context for the claim for better
    understanding of the question?

    The general theory is the Church–Rosser theorem:
    <http://en.wikipedia.org/wiki/Church–Rosser_theorem>

    If there exists a machine checked proof of this property for Haskell
    and to what degree, I am unaware of one. I suspect if it does exists
    it is specifically for a targeted subset that Haskell compiles to (System-F like?).

    For more information useful to this topic, I suggest taking a glance
    through SPJ's book IFPL:

    http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/

## chris glur — 2015-03-01 07:39:52

    ]> Where's formal proof of Haskell's claim to be able to avoid the need to

    ]> tell the machine what to do step-by-step, and just provide it with a

    ]> <description of the problem>, and allow it to workout/search for a route

    ]> to the solution?

    ]

    ] Do you have a specific quote in context for the claim for better

    ] understanding of the question?

    http://blog.wolfram.com/2015/02/11/qa-with-michael-tiller-

    author-of-modelica-by-example/

       Modelica is important because, as I mentioned previously, it

       captures a representation of people's models in an open way and in a

       way that can be reasoned about. This comes from the fact that

     =  Modelica is a declarative language, not an imperative language. When

       you deal with typical programming languages, the imperative

       constructs (e.g., do this, now do that, now loop until this is true,

       then overwrite that result) make it nearly impossible to actually

       extract the high-level intention of the user (at least not without a

       tremendous amount of discipline). Modelica is not a language of

       statements and operations, it is a language of relationship: how

       variables relate to each other through an equation, how the values

       of a variable are related to a type (and its physical units), how a

       resistor is related to a capacitor through connections in a

       schematic diagram. The point is that the structure of the model and

       all of these relationships are always preserved in Modelica.

       This property has been leveraged extensively to create very fast

       simulations by being able to reason about these relationships. We

       can see which variables depend on which other variables and use this

       to efficiently perform calculations, minimize the number of

       variables involved in solving nonlinear systems, recognize which

       signals are synchronized with other signals to ensure determinism in

       results, and so on.

    ----------------------------------------

    This chant which is apparently based on psychology/cognition is often seen.

    The above author is also unable to analyse his own mental processes,

    so he's just saying "it's nice" - in many words.

    Only recently, decades after grad: CS+Maths have I discovered the

    productivety of the composition of functions.

    Unfortunately, the syntax of unix piping is an ad hoc mess [as well

    criticised by Xhalee], but the economy of effort is remarkable.

    My analysis: why "it's nice"; is that it's cost effective of my effort/pain,

     because seldom do you need to abandon your invested effort and restart,

     [which IMO is M$ secret: DOS users could extend their investment to Win]

     because you can confirm the results at each of N stages,

     and the original cost of each of the functions is amortised over many jobs,

     [which is the tool box metaphor of unix].

    The details of <impedance-matching/currying> between stages etc, only comes

    after the TOP LEVEL justification has been stated; instead of starting with

    examples.

     Here's my latest example [to find the smallest *.nb in a big-dir-tree]:-

     list the zillion *.nb files in the dir-tree, showing their sizes

    + extract the size-field to the left [most significant] position

    + sort them

    + show me just the first 3.

    So there are only 4 concepts to burden the user.

    And the whole job can be progressively tested.

    A pointer from this forum, to a publication on the <effectiveness of

    combinators> which started correctly, by recognising the goal of labour

    saving, took as it's example: pretty printing; but unfortunately for

    me, is based on haskell tools. So I opened the haskell can-O-worms.

    So I want to know UP FRONT haskell's basis of it's claim to superiority

    over eg. Pascal.

    == Chris Glur.