Yoshiya@kt3kMay 20, 2024

ただ、実際の数学の教科書の証明を見ていると「○○の定理より〜」みたいな感じで、既存の定理を推論規則として使っている場面が良くあって、定理をただコピーするだけじゃなくて、推論規則として使えるようにするみたいな仕組みもあった方が便利そうなのだけど、定理が推論規則になるっていう状況があまりきちんと定義されていないような気がする


Yoshiya@kt3kMay 20, 2024

証明を static な木として記述させるとして、証明済みの定理をどうやって適用させるかがなかなか悩ましい。一番単純にいくなら、証明済みの定理をそのままコピーすることのみを許可する方法かな・・・


Yoshiya@kt3kMay 10, 2024

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


Yoshiya@kt3kMay 10, 2024

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.


Yoshiya@kt3kMay 10, 2024

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



Yoshiya@kt3kApr 19, 2024

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


Yoshiya@kt3kApr 10, 2024

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.


Yoshiya@kt3kApr 3, 2024

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


Yoshiya@kt3kApr 3, 2024

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

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


Yoshiya@kt3kApr 3, 2024

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


Yoshiya@kt3kApr 2, 2024

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



Yoshiya@kt3kMar 25, 2024

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

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


Yoshiya@kt3kMar 25, 2024

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


Yoshiya@kt3kMar 25, 2024

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


Yoshiya@kt3kMar 11, 2024

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



Yoshiya@kt3kMar 11, 2024

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


Yoshiya@kt3kMar 11, 2024

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



Yoshiya@kt3kMar 7, 2024

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

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


Yoshiya@kt3kMar 6, 2024

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


Yoshiya@kt3kMar 6, 2024

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



Archives