Re: does a table always need a PK?

Hi Heikki,

"Heikki Tuuri" <Heikki.Tuuri_at_innodb.com> wrote in message news:<gZG3b.333$st4.19_at_read3.inet.fi>...
> in computer science people usually think that a formal definition has to be
> mechanically verifiable, at least in principle.
>

Indeed, and where possible this should be the approach taken. The big challenge is, how do you get mathematics to say something in any way useful about things which are partially policy (backup) and partially down to greasy bits of machinery (tape drives) ? And what do you do in the mean time ?  

> Formal proofs of program correctness are too difficult for big programs,
Mmmm....

> but
> I have seen that for some details, writing a partial specification and
> proving the correctness in a mathematical fashion has uncovered bugs.
>

Absolutely. How's about this then; try implementing an RDBMS using Haskell. It's a functional programming language, therefore just some syntax sugar for the lambda calculus, and the act of doing this would probably force someone to come up with a mathematical model of what an RDBMS is. To some extent, anyway - you could probably express something about concurrency, transaction recovery and the like, but still not extend out as far as backups. (Alternatively, you could just specify the concurrent assignment of Tutorial D and do away with transactions ... :) )

It would also make MySql 6 a *truly* ground-breaking product, rather than more-and-less-of-the-same-old-thing.

• Tony