Path: text.usenetserver.com!atl-c01.usenetserver.com!news.usenetserver.com!atl-c05.usenetserver.com!news.usenetserver.com!postnews.google.com!75g2000cwc.googlegroups.com!not-for-mail From: "Marshall" Newsgroups: comp.databases.theory Subject: Re: A good book Date: 7 Jul 2006 00:19:43 -0700 Organization: http://groups.google.com Lines: 52 Message-ID: <1152256783.862429.279870@75g2000cwc.googlegroups.com> References: NNTP-Posting-Host: 24.4.95.46 Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" X-Trace: posting.google.com 1152256788 17973 127.0.0.1 (7 Jul 2006 07:19:48 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 7 Jul 2006 07:19:48 +0000 (UTC) In-Reply-To: User-Agent: G2/0.2 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.0.4) Gecko/20060508 Firefox/1.5.0.4,gzip(gfe),gzip(gfe) Complaints-To: groups-abuse@google.com Injection-Info: 75g2000cwc.googlegroups.com; posting-host=24.4.95.46; posting-account=s2xCFw0AAAD2mIwYYHAqjdsecwG0axmW Xref: usenetserver.com comp.databases.theory:156549 X-Received-Date: Fri, 07 Jul 2006 03:19:49 EDT (text.usenetserver.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. http://www.amazon.com/gp/product/3540208542/sr=8-1/qid=1152255760/ref=sr_1_1/002-4661063-2538456?ie=UTF8 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