JSR、自分の想像より遥かに多くの反響があって、なかなか面白い。npm のスーパーセットになるような、いろんなルールが科されているレジストリっていうのが意外とかなり需要があったらしい。
npm は良くも悪くも、ただのファイル置き場的な作りのままここまで来ていて、そのシンプルさで受け入れられたというのもあるだろうけど、JS の registry である事から期待される機能 (例えばドキュメント自動生成など) がおろそかになっていて、そこに対する innovation の余地みたいなところを JSR がうまく突いた形になったっぽい
SHEIN で 200~300円の時計4本と、1500円ぐらいの時計1本買ってみた・・・、どのくらいのクオリティなんだろう・・・? 🤔
ペアノ公理系で比較的簡単に証明出来そうな定理ということで、算術の基本定理を選んでみたけど、これでもちょっと複雑すぎる・・・
さらに落としてユークリッドの補題を考えてみたけどこれですら、どうやって主張を式に落とすのかなんだかよくわからない・・・
scrapbox 上で Peano playground というのを始めて、比較的かんたんな定理を完全に形式的に証明してみようと思っていろいろ作業してみたところ、自分は形式的に証明できる定理が何一つ無いということに気付いた。
メモ: 趣味プロの複数同時進行は良くない。1度に1つづつにした方が良い。
趣味プロなどで、プロジェクトがスタック気味になってきたら、プロジェクトの転用・目的の再定義に集中するのが良さそう。一番良くないのは、目的地が正しくない状態のままで速度が落ちた状態が続いてしまってモチベーション自体が下がってしまうこと。
今本当にやりたい事は Editor 関連と、proof verifier 言語になって来ているので、もう少しそっち方向へのコミットを増やしていきたい。
YAPC::Hiroshima に参加して色々リフレッシュできた。会期中に久しぶりに Code Golf (https://perlbatross.kayac.com/) に没頭出来て楽しかった。
Apple から PKL という設定言語が Open Source された。オブジェクトに型が付くというところは目新しいし、有用そうだけど、それ以外の機能、特に設定のテストを書きたくなってしまうようなやたら複雑な機能が多くて、個人的には設定で使ってみたい言語にはならなそうと思った。
久しぶりに flow type の contributor グラフ](https://github.com/facebook/flow/graphs/contributors) を眺めて見たけど、全く開発がスローダウンする気配が無い。世の中的には流行ってないけど、Meta 的にはきっとすごくアクティブに使われているんだろうなぁ