$ whoami

千秋

Independent Developer

I build systems where theory has to touch real code: functional programming, formal verification, compiler experiments, graphics engines, and practical automation. Currently looking for open source or development roles in Shanghai.

$ cat contact.json

location
Shanghai / Remote
writing
/blog

$ ls ./focus

  • Functional programming, type systems, and dependent types
  • Formal verification with Lean and proof-oriented engineering
  • Low-level graphics, WebGPU, WebAssembly, and engine architecture

$ tail -n 5 ./blog

Latest Posts

View all
  1. Tension Jul 29, 2026

    11 音 四级 可以用于 IV 大七 FM 7 ( 11 ) : F A C E B 紧张感 由于升四度,有千与千寻的感觉(?)神秘的神隐感 可以用五级六级和弦保持这个4音 终止的一级可以加入 11 有奇妙的氛围感,很不和谐。 加在属...

    /blog/04_音乐/tension
  2. lean Jul 29, 2026

    结构体默认值 haskell structure Box where m := 0 def b : Box := {} eval b { m := 0 } 默认值语法 State Monad 本文假定你对 Monad 有了解,只需要知...

    /blog/05_计算机/lean
  3. nixos Jul 29, 2026

    https://nix.dev/tutorials/nixlanguage.html module 一个简化的 Nixpkgs Module 结构如下: typescript {lib, config, options, pkgs, ...

    /blog/05_计算机/nixos
  4. Hessian Matrix & SVD 分解 Jul 29, 2026

    梯度告诉你往哪边走。 Hessian 告诉你每个方向弯得多厉害。 SVD 把一个线性映射拆成:正交变换、沿坐标轴伸缩、再做一次正交变换。 Hessian 描述函数的局部形状。SVD 描述矩阵怎样变形空间。二者在最小二乘中接到一起。 H...

    /blog/07_数学/hessian-matrix--svd-分解
  5. 半角公式 Jul 29, 2026

    gg (4 封私信 / 2 条消息) 半角公式的推导(超详细版) 知乎 一、半角公式 $$ \sin\frac{\alpha}{2}=\pm\sqrt{\frac{1\cos\alpha}{2}} $$ $$ \cos\frac{\a...

    /blog/07_数学/半角公式