Writing is hard

I have had real difficulties with writing anything at all. A terrible version of a writer's block has taken over me - it affects writing code, doing math and even writing poetry. I've done almost nothing at all for a while now. Solution I came up with is hardly original, but I do hope it will help me with writing.

Simple solution is decreasing my inhibitions about writing so that at least I will write something every day and preferably I will try to write something in every language I can reasonably well write at all - which would mean writing in finnish, english (maybe swedish), Haskell and Scheme. Perhaps I will include Java, C/C++ and Coq to that list. Java because I am trying to write little helper functions to wonderful space strategy game called Planetary Hoppers. C/C++ because it's language I actually don't know very well and that I would like to toy with (especially with it's exceptions and unsafe commands and all that fun stuff). Coq would belong to that list just because it is language I am trying to learn at the moment, but I am lazy and I don't think SICP approach will be optimal for toying with coq. I will try to write about 1000 words about anything at all in any natural languages in that list and couple neat functions in any programming languages in that list every day. So that is that.

I am thinking about writing something about poker here as Michael Halila borrowed me couple of books about poker and I finally got around reading half of them (Dummies was very quick to read - I read it in about 5 hours. Sklansky seems like fun book so far). At the moment 7-card stud and texas hold'em are my favourite games.

Coming soon: Planetary Hoppers, Poker, random-stuff-that-I-like

The Coq proof assistant

I must admit that I really like the Coq - it's terrific tool that already feels rather nice even though I haven't got much experience with it. It can be used as a proof assistant in proving theorems in Calculus of inductive constructions and as a tool for building verified programs. I plan to explore its reach more completely in later posts after I've played with it more.

Here's example from the Coq's standard library:

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Definition pred (n:nat) : nat := match n with
| O => 0
| S u => u
end.

Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
simpl; reflexivity.
Qed.


This is pretty much normal way to define natural numbers as zero and its successors. In coq this means that we are defining this type called nat that nat is either O or successor of a nat. Inductive in the beginning means that this definition declares way to construct instances of this type - which in turn means that coq will produce nat_ind, nat_rec and nat_rect - way to do inductive statements and recursive operations on nats. Definition of predecessor function is very straightforward and theorem of every natural number being predecessor if its successor is also easy to read even if one might not know what simpl and reflexivity are - they are called tactics and proofs in coq are build from them.

The Coq tutorial was rather nice introduction if rather short and now my prime source of information about the Coq are its reference manual and standard library - both of which are rather readable and intresting even though I have just started learning coq. Other people have written about it much more elegantly, but since this is learning experience it doesn't really matter.

I must admit that the french can name things well - I mean what would be better name for a tool?