Is someone over 80? A calendar question, answered with every day counted.
age.pl · output · proof · check · try it in the playground
Pat was born on 21 August 1944. Some benefits, discounts or rules start “after your 80th birthday”.
On 1 October 2026, is Pat older than 80? It sounds easy, but calendars have leap years, months of different lengths and birthdays on 29 February. We want an answer that shows its arithmetic.
Two facts: a birth date, and the date we ask about. Writing the date down (instead of reading the computer’s clock) means the answer is the same tomorrow.
birth_date(pat_h, date(1944, 8, 21)).
as_of(date(2026, 10, 1)).
true :+ age_above(Person, years(80)).
The last line is the question: find every Person whose age is above 80
years. :+ means “work this out and report what follows”.
The rule for “older than N years”, quoted from the program:
age_above(Person, years(Years), Date) :-
integer(Years), Years >= 0, birth_date(Person, Birth),
date_day(Birth, Born), date_day(Date, Today), Today >= Born,
anniversary(Birth, Years, Anniversary), date_day(Anniversary, Threshold),
Today > Threshold.
In words: turn each date into a day number (days since the start of the
calendar), find the 80th birthday, and check that today is strictly later.
date_day is defined in the same file, leap-year rules included.
age_above(pat_h, years(80)).
Yes: Pat is older than 80 on 1 October 2026.
The proof records every number it used:
Along the way it shows why 1944 and 2024 are leap years (divisible by 4, not by 100) and why 2026 is not.
A separate checker reads the proof against the program:
mod) is
recomputed by the checker and agrees;Verdict: checked. All 54 steps verified, nothing taken on trust.
node bin/eyedia.js examples/age.pl
node bin/eyedia.js --goal "age_above(pat_h, years(80), date(2024, 8, 22))" examples/age.pl
node bin/eyedia.js --goal "age_days(pat_h, date(2026, 10, 1), Days)" examples/age.pl
The last one answers age_days(pat_h, date(2026, 10, 1), 29991). Change as_of to date(2024, 8, 21),
the 80th birthday itself: there is no answer, because on that day Pat is
exactly 80, not above 80. One day later, the answer comes back.
Date arithmetic is where small mistakes hide. Here each day number, each leap-year decision and each comparison is written down and rechecked, so a “yes” can be audited down to the last day.