Re: A good book
Date: 7 Jul 2006 00:19:43 -0700
Message-ID: <1152256783.862429.279870_at_75g2000cwc.googlegroups.com>
Chris Smith wrote:
>
> Let's say you met someone who has a strong mathematical background, a
> long history of development of mainly business application software, a
> perfectly fine understanding of writing SQL queries in practical
> settings. This person understands that OO languages are somewhat
> arbitrary, but not particularly convinced that they are evil.
> Similarly, he is not convinced of the need for writing significant
> amounts of code in declarative style, nor that the existence of a simple
> formal mathematical model behind relational databases is necessarily
> exploitable to produce better software. Let's further say that you
> could get said person to read one book. What would it be?
>
> (Yes, this is somewhat autobiographical...)
Chris,
Your question was quite interesting.
I have a crazy idea for an answer. Rather than being a response to what you specifically asked for, I'm instead riffing off of the phrases "formal mathematical model" ... "produce better software."
The book is "Interactive Theorem Proving and Program Development" by Yves Bertot and Pierre Casteran.
Now, I will just come right out and admit that I haven't been able to make it through this book yet, so my recommendation is based on somewhat vague impressions and the earlier chapters. Alas, my time for serious study is quite limited, and this book demands serious study.
Anyway, the book is about the Calculus of Inductive Constructions, and specifically the Coq proof assistant.
Background reading:
http://en.wikipedia.org/wiki/Coq http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory http://en.wikipedia.org/wiki/Calculus_of_constructions
Some of the most interesting stuff going on in type theory right now (IMHO) and fits beautifully with relational theory. In particular, it is the only type system I know of that can express the type of the natural join.
Marshall Received on Fri Jul 07 2006 - 09:19:43 CEST