As one of the first 250 to learn Dartmouth BASIC in prep school in NH in 1964 using a teletype machine direct hook up to Hanover, I proffer my congratulations also.
Out of the Dartmouth GE Time-Share Multics came the name of Unix for one person.
Please see my Ada 95 post here today, but be advised that there is no proof in mathematical logic for the pre- and post-conditions reincarnated by Meyer in Eiffel (from Hopper in COBOL) and then copied by Barnes into SPARK. Hint: the problem is still in rendezvous with costly locks and unlocks, and not resolved appropriately in Ada 2022.