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