I feel like I don't have much to say most of the time - which is rather huge problem for a starting blogger. Easiest way out is of course to describe all wonderful thoughts that have crossed my mind during the day which would fill this blog easily enough - only problem is that I would prefer having something worth saying.
Now I do have something of a plan - I intend to read SICP again, but this time I will use Coq as language of implementation so that I learn to use Coq and its intresting extraction facility. In essence I will prove theorems about some types and use Coqs extraction command to produce Scheme code. Now I do expect this to be a little bit harder than what it was to read through SICP using Scheme or Haskell, but I expect it to teach me a lot about using Coq as specification tool and proof assistant.
SICP is my favorite CS-book, because of its clear approach to foundations of programming. It does have its critics (pdf) and HtDP seems to have advantage over it when taught in CS101 courses.
There's still a lot of doing left before I can claim any basic understanding of coq - which is very point of my SICP project.
No comments:
Post a Comment