今年の目標を立てる。資格、プログラミング、形式手法、文化、健康、それらに関して目標を立てた。

資格

基本情報技術者試験と応用情報技術者試験を受けようと思う。

スタートアップ企業で色々やっているが、結局、基本的な知識が足りないのではないかと思っている。例えば、BGPとかもよくわかっていないし、アジャイルとかもよくわかっていない。

ある人は高度情報処理技術者試験を受ければいいのでは、と提案してきてくれたが、上記の自分の知識不足に対する不安があるうちはそれに挑戦できそうにない。この不安は大きく、何に対しても躊躇してしまい、AWSのあれこれとかを受ける気力が湧かない。実績という生の事実ではなく、資格という形式的な事実が欲しい。

あとは、転職をする際に、最低限の知識がちゃんとあることを証明できる証拠が欲しい。 (会社にキャリアアップのための補助金を制度として導入してもらうようお願いできたら、いいな。)

プログラミング

Rustの勉強を続ける。

今年は、Isabelleの勉強を引き続きする

昨年は、Lamportの Specifying Systems を読み終え、TLA+の基本的な文法の学習を終えた。

TLA+については、分散システム周りでの活用がより見込めるが、分散システム周りに関する興味がそれほどないことが判明した。いくつかの種類のPaxosに関する論文を読んだが、それほど私の琴線に触れるものではなかった。

今は Concrete Semantics を186ページまで読んでいる。ただ、練習問題はほとんど解いていない。

そこで、証明力やIsabelle力を高めることに注力したい。

完全正則性と一様化可能性との同値性などの基本定理の証明がないなどの課題がIsabelleではあるらしく、それの提案を友人から受けた。

そういうわけで、IsbellのUniform Spaceを読んで、形式化しようと思う。

いい加減、装甲騎兵ボトムズを履修しようと思う。

ペールゼン・ファイルズが、入門としてはちょうどいいらしいので、そこからスタートしよう。

肝機能を改善する。

食事、運動、睡眠を規則正しくする。