Proven correct receipt module

Question

I'm working on a register which produces receipts when customers buy articles. As an exercise, I'm thinking about making a receipt module in Coq which cannot produce erroneous receipts. In short, the articles and the payments on the receipt should always sum to 0 (where articles have price > 0 and payments have amount < 0). Is this doable, or sensible?

To do a quick sketch, a receipt would consist of receipt items and payments, like

type receipt = {
  items : item list;
  payments : payment list
}

And there would be functions to add articles and payments

add_article(receipt, article, quantity)
add_payment(receipt, payment)

In real life, this procedure is of course more complicated, adding different types of discounts etc.

Certainly it's easy to add a boolean function check_receipt that confirms that the receipt is correct. And since articles and payments always is added in runtime, maybe this is the only way?

Example:

receipt = {
  items = [{name = "article1"; price = "10"; quantity = "2"}];
  payments = [{payment_type = Cash; amount = (-20)}];
}

Is it clear what I want?

Or maybe it's more interesting to prove correct VAT calculations. There's a couple of such properties that could be proven.

Answer 1

You can use Coq to prove your program has properties like that, but I don't think it applies to the particular example you have presented. Articles and payments would be added at different times, so there's no way of garanteeing the balance is 0 all the time. You could check at the end if the balance is 0, but the program already has to do that anyway. I don't think there's a way of moving that check from execution time to compile time even with a proof assistant.

I think it would make more sense to use Coq to prove that an optimized and a naive implementation of an algorithm obey the same input / output relation. If there were a way to simplify your program, maybe at the cost of performance, maybe you could compare the two versions using Coq. Then you would be confident you didn't introduce a bug during optimization.

That's all I can say without looking at any code.