Natural numbers should start with 0 [0].
Suspiciously, the following lines in the proof can be entirely removed while still verifying:
@func nat(x any) bool;
term 1 nat;
> Natural numbers should start with 0 [0].
I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up going with 1 is we were imitating the structure of the proofs in Landau's "Foundations", and he uses 1 as his first number.
An interesting takeaway was the following. The way he structures his theorems and proofs, he makes use of his assumption that 0 is not a natural number. For example, Theorem 7 in the book is "y != x + y (for all natural numbers x, y)". So I found that sticking to my roots as a programmer (and admirer of Dijkstra) and insisting on zero-indexing led to more complicated theorem statements (e.g. "y != x + y for all natural numbers x, y > 0"). I'm not sure whether this is something structural about how the properties of natural numbers, integers, etc. relate; or whether it's an artefact of Landau's approach.
> Suspiciously, the following lines in the proof can be entirely removed while still verifying:
Suspicion warranted! The first (or zeroth) of these is a bug we hadn't fixed yet (see [1]). Our implementation is rather rough around the edges, but I've put a small fix for this—try again and tell me what you think.
The line "term 1 nat" interestingly isn't used in the theorem we've written, so it's more a mistake on our part for including it in the sample code. Good spot! See the language page [2] for an example where it is used.
As an aside, have you noticed that our proof style is based on what we call "Dijkstra-chaining"? Any thoughts on this? [3]
[0] https://paste.sr.ht/~akiarie/d7a2ae368faae4ba9a8bc13eeefcf18....
[1] https://todo.sr.ht/~lbnz/i2/1
[3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E...
Difficult to convince the entire field of mathematics that they are wrong though. It's hard enough to convince programmers - humans just have first=1 drummed into us so much it's like trying to convince a stone age man that the world is round.
I think mathematicians care even less because most of the problems with starting from 1 can be hand waved away when you're just writing non-executable formulas and can make up any syntax you want on the spot. If anything is really awkward with 1-based numbering, just change the notation so that it isn't! Programmers can't really do that so they feel the pain more.
(For the record I think all the arguments Dijkstra gives for 0-indexing are correct. I just lack the mathematical intuition to see why the special case above appears to be one in which admission of 0 as complicates things.)