A non-interactive, binary relational database programming language is designed using formal specification. The design is conducted using the Vienna development method. The underlying data model is made as general as possible so as to minimise the restrictions placed on the database user. In contrast to the normal method of handling database integrity constraints by dynamic checking, constraints are regarded as assertions, and proofs of correctness based on Hoare-style axioms and proof rules are used to show that semantic integrity is maintained.