For Me in Twenty Twenty-Three

Let’s get this over with!

Every year I task myself with a list of publicly declared goals,¹ and then in the next year, if I find myself among the living,² I grade myself. How did 2022 go? Let’s start with my small goals.

1. Goal: Observe as many Messier objects as weather permits and get my RASC certificate.

Well, I did not get my RASC certificate but I made progress. Meridian’s skies are often overcast and even when clear, are horribly light-polluted. I figure I can only naked-eye magnitude 3 or 4 stars from my backyard. When using my binoculars or telescope I estimate I lose two or more stellar magnitudes to light pollution. Bright, magnitude 8 or 9 Messier objects, that are easily seen with binoculars from dark sites are not visible in my backyard. It’s frustrating. Urge to kill rising! To make a dent in my list of missing Messiers I will need to seek out dark skies. For 2023, I am repeating this goal; I will keep looking until I complete my Messiers or expire. As for my “grade,” I’m giving myself an Incomplete.

2. Goal: Learn more proper northern hemisphere star names.

I am pursuing the quixotic quest of stepping outside on my patio and calling out the visible “named” stars. This is a rare astronomical task that light pollution helps; it greatly reduces the number of stars you must name. I am making slow progress. I can already achieve this goal on some nights, especially partly overcast nights, as only the brightest planets and stars can be seen. For 2023 I will increase my efforts and cultivate some productive habits like looking up the ten brightest named stars visible from my backyard on given nights. I’m giving myself another Incomplete.

3. Goal: Continue shooting and adding captioned images to my pictures site.

In 2022 I set an all-time captioned image upload record. I wrote almost as many caption words³ (about 50 pages), as blog words (about 60 pages). Many 2022 pictures came from our Australia and New Zealand trip. But, importantly, I more than met my goal. I’m giving myself an A+. For 2023 I am not setting an image quota. I will upload pictures when the whim strikes.

4. Goal: Read at least ten books.

I read twenty books so I’m giving myself an A. For 2023 I am not setting any reading goals. I will read what I read.

5. Goal: Blog more!

In 2022 I cranked out 19 blog posts: not great, but better than many previous years. I’m giving myself a C+. For 2023 I am planning to break my all-time blog post record. In 2012 I wrote 37 posts, so I have to hit 38.

That completes my small goals for 2022. In 2023 I’m adding one additional small goal.

6. Goal: Weigh 85 kilograms or less on December 25, 2024.

For the last two years, I have been slowly losing weight: currently, I’m at 88 kilograms. I haven’t been making an effort to lose weight, it’s a consequence of walking a lot, and staying on the Mali diet. The Mali diet is super-heathy, anyone that stays on it will lose weight. I might as well make it a little goal.

Now let’s address the Humpback in the Sea. How did I do with my primary priority project which was:

7. Whale Goal: Write a first draft of a short book that uses LEAN to formally prove some school geometry theorems.

I’ve written a fragmented partial draft and I’ve made headway on the thousands of little things you must do to write a book about software, mathematics, and history but overall, I have failed — abjectly! I’m giving myself an F+. I am not giving up! I will continue working on this project in 2023 but I’m changing how I swim after this whale.

To start, I am going to write some typical programs in LEAN4. The LEAN type system is powerful enough to formally prove advanced mathematical theorems. This distinguishes LEAN from most programming languages and tells this old polyglot programmer that “LEANish” languages represent something new and important. Most mathematicians using LEAN focus on formal theorem proving but my tiny naked ape brain may have better luck with prosaic “hello world” applications. As I work out some LEAN programs I will post them here.

Finally, I’m going to take Roy Peter Clark’s advice (see Writing Tools) and write about the problems I face while working on my draft. I’ll use this blog as a test site, sounding board, whipping post, and confessional as I foolishly attempt to outswim a whale.

Overall, I’m rating 2022 as a D+ year. I will make efforts to improve, and if in 2024 I find myself among the living, I will tell you about it.

---

1. Private goals can be conveniently memory-holed.↩︎

2. At my age this cannot be taken for granted.↩︎

3. I call them milliblogs.↩︎