Yoshiya@kt3kJun 22, 2024

AI のサブホスティング的なサービスは基本全部はやらない気がするなぁ・・・

AI を使っていると分からないように AI を裏で使っているサービスは強そう

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 が何だかすごくよく見えるなぁ。ベゼルに丸い計算尺をデザインとして付けているというのが何だか分からなくてすごい