Yoshiya@kt3kJun 26, 2024

cell を使って、新しい frontend の趣味プロを始めた。

2d canvas に 60 fps で色々描画するタイプのプロジェクト。main ループで取れた fps 値を遠隔地のラベルに表示するというところで、cell 制作時構想していた pub/sub パターンが綺麗にハマってとても気持ちが良かった。


Yoshiya@kt3kJun 26, 2024

capsidcapsule の後継プロジェクトとして cell を作った。

capsule の interface を組み替えてより自然な形に組み立て直したもの。関数1個を1つのコンポーネントにするというアイデアは、最近の React から拝借した。

React に限らず Solid や Qwik なんかも、1コンポーネント = 1関数というデザインを踏襲するようになってきていて、フレームワークを超えて共通のパターン言語のようになって来ている気がしたので、このデザインにしたかった。

一番実装が難しい on helper とか初回登録時のロジック部分はほぼそのまま capsule から拝借して来ているので、フレームワーク自体はほぼ1日ぐらいで完成。テストケースを追従するのにさらに1日。TodoMVC を移植するのにさらに1日ぐらいの作業量でほぼ完成できた。

TodoMVC を cell で実装してみたところ、全体のバンドルサイズが 2.38 kB になって、capsule の時よりさらに 1kB 程度小さくなった。自分が知る限り飛び抜けて最小サイズで TodoMVC が実装できていてとても気持ちが良い。


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



Archives