NORQAIN って全然ピンとくる時計がない。その割に OMEGA ぐらいの値付けがされてて、全然理解が出来ない

Many books try to capture a proof as a sequence of inferences on statements. It looks natural at first because it is similar to how we make arguments in natural languages, but it is not natural as it looks.

If you try to formalize a proof in that way, the proof internally have to have a lot of backward references to indicate what inference uses what statements. This backward reference structure instantly becomes hugely convoluted, and it makes the proof cluttered and unreadable.

A proof should be considered as a static tree, instead of a series of dynamic operations on statements.

Node 結構 Deno を追って色々な機能を入れたけど、結局 Node = 設定が面倒、Deno = 色々入ってて楽、っていうポジショニングはあまり変わっていない気がする。

Val town raised 5.5m. It (probably) uses Deno internally. The root concept, learnable programming or end user programming, is very interesting and the product itself looks interesting. However I think it has many problems in design:

(1) The language itself is too complex. I don't think end user consider this as learnable.

• JavaScript itself is too advanced language to the learners, and Val Town environment is not a good starting point for learning JavaScript (Browsers or local runtimes are better because of the availability of huge documentations, tutorials, blog posts, books, etc).
• Dependency to npm ecosystem, or Deno ecosystem is further complex to the learners, and it's nearly innaccessbile to them in my view.

(2) Deployment concept in val town looks too abstract and too complex.

• A deployment can have any interface. This makes the orchestration of deployments very difficult. If you want to connect 2 deployments, you probably needs glue code for it. If you connect 3 deployment, you'll need 3 glue codes. For 4 deployment, 6 glue codes. For N deployment, N(N-1)/2 glue codes. This doesn't scale well.
• The system should provide some standard interfaces for communication between deployments.

(3) Deployment can't be tested in isolated way.

• This might be improved in the future, but currently there's no way to unit test them. This prevent the users to develop complex thing.

The 3rd point is currently the blocker for me to use it in a serious way.

Formal system はシンプルであるべきだと思いつつも、自分がやっている複雑な推論は認識したがらない・目を向けたくないという性質が人間にはあって、その結果自分が普段使いできるような Formal system を誰も定義しようとしない

Formal system は色々と定義されている (ZFC, NBG, Peano axioms, ETCS, LK, etc) のに誰もそれを使って証明しないのはそれらの言語が人間が直接使うには原始的すぎて、普段やっている証明とかけ離れすぎているから、というのがあると思う。

普段使いできる Formal system であるためには、もっといろんな推論が出来ないといけない。けど、普段やっているような推論を Formal system に入れるためには、ものすごい複雑な定義が必要になってしまうので、誰もやらない

Formal proof で証明出来たものが数学の定理であると定義するのは良いんだけど、誰も実際それで証明してないという大問題がある

Breitling の Navitimer が何だかすごくよく見えるなぁ。ベゼルに丸い計算尺をデザインとして付けているというのが何だか分からなくてすごい

TISSOT PRX は試着してみた結果自分の普段着と全く合っていない事が分かったので、路線を変えて、むしろドレッシー路線のスイス時計を探す事にした。

結局、TISSOT の別のモデルの Le Locle というのが一番あっている気がしてきて、その時計がたまたま Fashion Valley の Bloomingdale's の一階の時計売り場にあったので、そこの Christopher という店員から購入した。Christopher は時刻合わせの仕方等を丁寧に教えてくれるとても良い店員だった。

GCS って極端にスパイクすると Rate Limit に引っかかるから、ある一定のレート以上でスパイクしないようなキューイングが必要らしい・・・(レートリミットはハードコードされてる訳ではなくて、一定時間そのスループットを出したらレートリミットがじわじわ上がる、みたいな複雑なレートリミットがあるらしい)、ある程度のスループット以下の使い方なら問題にならないんだろうけど、正しく使うのが難しすぎる気がする・・・

Furlan Marri というブランドが相当良いらしい。サーモンダイヤルのやつとか結構欲しいかも

Peano Axioms

休日用は BALTIC の Hermetique Tourer か MR01 で迷う・・・、ぱっと見は Hermetique Tourer が好きだけど、MR01 も十分カッコいいのと、MR01 はマイクロローターなところが好き。ただ、MR01 はちょっとドレッシー側に寄りすぎてる気もする

欲しい時計、平日用 TISSOT PRX Powermatic 80 40mm Blue dial

一番調子が良い時は TODO リストなんか作らなくても、やる事が思い浮かぶ -> やる -> やる事が思い浮かぶ -> やる -> ... っていうループが勝手に回る

欲しいものがありすぎる状態は、欲しいものが全くない状態よりはよっぽどマシだ

App idea: Good, Bad, Tomorrow

JSR、10年間 innovation が起きていない registry に innovation を起こすため、というフレーミングもうまく機能している気がする。

確かに Deno がそれを始めた理由は semver の dedupe をする手段がないから、というのがきっかけではあったのだけど、せっかく registry を作るのだからということで盛りに盛った新しいアイデアが当初のモチベーションを完全に塗りかえてしまって、JSR は JS のレジストリエコシステム全体に対する革新なのだ、という新しい旗があまりにも綺麗にはためいて、JSR とはそもそもそういうものだったのだという説明に Deno 自身ですら納得し始めてしまっている。

JSR、npm と互換性がありつつ、デメリットがかなり少なくて(利用側への負担がかなり小さい)、尚且つハッキリとしたメリットがある(API doc 自動生成、.js, .d.ts 自動生成)ので、これはかなり筋が良いのではないかという気がしてきた。

時計界隈、車界隈より遥かにプレイヤー数もモデル数も多くて、見ていて飽きない。面白い。