# Formal proofs via 'joy' or any system?

## chris glur — 2014-11-06 17:20:40

    Cc: ETHO forum.

    Re. "rock solid"/reliable software:

     Ada had that declared aim. Is it still alive?

     Wirth advocated simplicity; if the whole-picture is small enoungh,

        you can *see* the faults. But few tasks can be kept small enoungh.

     Eiffel introduced checking mechanisms beyond strict typing, but nobody

      seemed interested.

    There's been talk/research about formal methods: where you could "prove

    the results, via algebraic manipulation of the code". Or better still have the

    computer auto-prove the code.

    Searching the literature in this direction I came across repeated claims

    that certain functional languages could formally prove correctness via

    algebraic manipulation of the code.  Several examples of manipulating

    the code of the language: joy; were published, but I never saw a complete

    task being proved.

    It seems like the Artificial Intelligence wave of the 70's: they eventually

    settled for expert-systems, which works more like a horse-and-rider.

    I.e. the user and system collaborate.  Which is where ETHO has been for

    decades.

    What did we call those low-flying-missiles, which automatically found

    their targets, and have now been replaced by horse-and-rider drones?

    == Chris Glur.

## John Nowak — 2014-11-18 16:25:50

    On Nov 6, 2014, at 12:20 PM, chris glur crglur@... [concatenative] <concatenative@yahoogroups.com> wrote:

     > Searching the literature in this direction I came across repeated claims

    > that certain functional languages could formally prove correctness via

    > algebraic manipulation of the code.

     There are more than just claims, you'll be happy to know!

    Richard Bird and Jeremy Gibbons have done a lot of work on this topic. Bird's "The Algebra of Programming" is possibly the best book to pick up, but it can be hard to find for a sane price. This paper by Gibbons appears to be a good proxy:

    http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf

    If you've not read it yet, you should also read Backus's famous paper for some of the origins of the idea of calculating programs:

    http://web.stanford.edu/class/cs242/readings/backus.pdf

    I'd also look at categorical programming languages like Charity. The paper you want to read is called "Charitable Thoughts", but it may be hard to find in the sea of academic FTP wastelands. If you can't dig it up somewhere, let me know and I'll send you a copy. (I can't at the moment due to being at work.) You can also look at Hagino's thesis on the topic:

    http://synrc.com/publications/cat/Category%20Theory/Type%20Theory/Hagino%20T.%20A%20Categorical%20Programming%20Language.pdf

    Of course, if you really want to prove non-trivial things (e.g. "my red-black tree implementation is actually self-balancing"), you're not going to be doing it algebraically. You're going to be using constructive proofs and a language like Coq. If you want to learn more about how to do such proofs, read this book by Adam Chlipala:

    http://adam.chlipala.net/cpdt/

    If you're serious about wanting to prove things formally, the tools are already there. Go use them and show us all your cool stuff!

     > Several examples of manipulating the code of the language: joy; were published, but I never saw a complete task being proved.

     In my humble opinion, concatenative languages are not great for algebraic manipulation. The problem is that the stack is threaded through every function (more or less), and this makes it very difficult to reason about things in isolation.

    If you want a concrete example of the problem, try writing a version of the 'map' function in Joy such that it has the following semantics; you'll see it's not as easy as it looks:

       forall F G. [F] map [G] map == [F G] map

    (Someone may object to this example because 'map' in a concatenative language is typically equivalent to a combination of 'map' and 'fold'. Given that the accumulator passed to such a map/fold is the *entire state of the program*, I hardly think this makes things better!)

    - jn