I've been going through the Hyperbook and some of Dr Lamport's writings and talks and finding them all very inspiring.
In parallel to this I have recently started to study category theory, and I've read that Joseph Goguen said that CT is a natural language for software specification.
Maybe. I won't argue about that. But a simple look at haskell where they often use categorical concepts let
me think that all that may be very tricky.
It is not enough to have a general method in computer science nor a good language with a good
manual you also need a comprehensive treatise that explains how to make the tools you need. Even a descent
recursive parser may be tricky. There are condition about the acceptable grammars and so on.
There are comprehensives treatise for imperative languages: Knuth and Grune. But outside, it is just like a desert. Only
sparsed things about object languages, sparsed things about functional languages, sparsed things
about algebraic data. And I think there are no honest comprehensive things about categorical things or
parallel things...
And to prove an algorithm it is not better. Proving simple things is simple. But when things go recursive, it is
less simple and I'm afraid that if you want to turn to categorical (and then somewhat abstract) things
well... I prefer not scaring you.
--
FL