Niri v26.04：Wayland 合成器加入背景模糊、ext-background-effect 協定、GPU 效能重構
niri-wm/niri GitHub Releases · 2026-04-26
Niri 是以 Rust 撰寫的「可捲動平鋪」Wayland 合成器——視窗排列在一條向右延伸的無限帶上，開啟新視窗不會使現有視窗縮放。v26.04 是 2026 年 4 月的月版本，最低支援 Rust 1.85。
背景模糊與 ext-background-effect 協定
v26.04 最重要的新功能是背景模糊，透過 Wayland ext-background-effect 協定實作——應用程式可宣告請求模糊，無需額外 niri 設定。合成器提供兩種模式：
- Xray blur（預設）：在第一幀渲染時計算模糊後的壁紙，後續幀複用，適合靜態壁紙，GPU 開銷低。
- Normal blur：在每幀渲染中途讀回已渲染的像素並套用模糊，適合動態背景（如播放中的影片壁紙），但每幀有額外 GPU readback 開銷。
已支援此協定的應用：Dank Material Shell、Noctalia、foot terminal、kitty、Ghostty。
渲染架構重構
v26.04 將渲染清單（render list）的建構從 pull-based iterator 模式重構為 push-based closure 模式，在典型工作站上帶來 2–3 倍效能改進，在舊款 Intel 筆電上高達 8 倍。合成器同時整合了 Tracy GPU profiling，支援 GPU zone 視覺化以分析模糊等高開銷特性的效能瓶頸。
錄影（Screencasting）改進
新增游標元資料（cursor metadata）支援：合成器以獨立元資料流傳送游標位置而非直接嵌入影格，讓 OBS 等錄影軟體可自行控制游標顯示。新增 niri msg casts 命令查詢進行中的錄影，以及 IPC 事件訂閱介面。解決了 Microsoft Teams 的相容性問題：串流啟動延遲到第一個錄影目標被選擇後，避免 Teams 取用空串流。
設定增強
optional=true 標記的 include 區塊在目標檔案不存在時不報錯；路徑支援 ~ 展開；新增 popups 設定區塊讓 pop-up 選單可獨立設定透明度與背景效果。
HardenedBSD 正式遷移至 Radicle 去中心化 Git 平台
HardenedBSD · 2026-04-26
HardenedBSD 安全強化版 BSD 作業系統宣布正式將其原始碼倉庫從 GitHub 遷移至 Radicle——一個以點對點（P2P）網路為基礎的去中心化 Git 協作平台。
Radicle 的技術架構
Radicle 以 Heartwood 協定為核心（以 Rust 撰寫），每個倉庫以 Radicle ID（RID）識別，格式為 rad:z<hash>。倉庫資料透過 gossip 協定在節點間傳播，不依賴中央伺服器。貢獻者透過 rad CLI 工具克隆與推送，可在無網際網路連線的本地網路上同步。Issue 與 Patch（pull request 等價物）也以倉庫內的資料結構儲存，不依賴平台服務。
遷移動機
HardenedBSD 的安全強化定位（ExecShield、SafeStack、PIE 預設啟用、CFI）與去中心化自主的工程哲學相符。GitHub 對伊朗、敘利亞等被制裁地區開發者的帳號限制事件（2019–2023 年間曾有多起報導）以及微軟所有權，是此類專案考慮自主託管的常見動機。
對貢獻者的影響
現有 GitHub 鏡像繼續維護，使用 git clone 的用戶不需立即更換工具。主要活躍開發者和希望提交 Patch 的貢獻者需安裝 rad CLI，設定本地節點，並透過 Radicle 網路提交。Radicle 的生態系尚不成熟（無 Actions CI、無 GitHub Pages 等平台服務），HardenedBSD 的 CI 需要自行架設。
「為什麼不用 Lean？」——Isabelle 創造者論兩大定理驗證系統的技術差異
lawrencecpaulson.github.io · 2026-04-23
Isabelle 定理驗證系統的創造者 Lawrence Paulson 在 個人部落格中回應「為什麼不直接使用 Lean？」的問題，從型別系統設計、自動化能力與易讀性角度比較兩個系統的根本差異，引發形式驗證社群熱烈討論（HN 243 點、Lobsters 21 點）。
型別系統的根本差異
Lean 4（與 Coq、Agda 同屬）使用依賴型別系統（dependent type theory）：型別可以依賴值（如 Vector n 的長度 n 是型別的一部分）。Isabelle 則以 Simple Type Theory（HOL，Higher-Order Logic）為基礎，刻意避開依賴型別。
Paulson 指出依賴型別帶來的實際痛點：型別等同（type equality）的判定依賴「相等性」的定義，而直覺型別理論（Intensional Type Theory）中 T(N+1) 與 T(1+N) 是不同的型別，即使數學上等價，使用者需要插入轉換（coercion）才能讓程式通過型別檢查。此問題在處理數學索引（如矩陣維度、多項式次數）時尤為突出，是 Lean 初學者的主要困惑來源之一。
自動化：Isabelle 的 Sledgehammer
Isabelle 的 Sledgehammer 呼叫多個外部自動定理證明器（ATP：Vampire、E、CVC4 等）嘗試自動完成當前目標，成功時生成一行 Isabelle 策略（by (metis ...)）。Paulson 認為「Lean 沒有任何可比擬的工具」——Lean 的 decide/omega/simp 等策略功能較有限，不及 Sledgehammer 在數學定理證明中的廣度。
Isabelle 的 LCF 架構與 Prop 效率
Isabelle 採用 LCF（Logic for Computable Functions）架構：核心型別系統保證所有定理均由小型推論核心產生，不儲存完整的 proof object。Paulson 主張對於具 Prop 排序（proof-irrelevant propositions，即命題的所有證明等價）的系統，儲存巨大的 proof term 是浪費，Isabelle 的設計更為精簡。
Quarkdown：Markdown 超集語言——腳本、版面配置與演示文稿生成
quarkdown.com (HN) · 2026-04-27
Quarkdown 是一個以 Kotlin JVM 實作的 Markdown 超集語言，在 Hacker News 以 236 點登上前頁。它在 CommonMark 基礎上加入腳本執行（scripting）、自訂佈局（layouts）、數學排版與 PDF/HTML 演示文稿生成能力，目標是以文字標記格式取代 LaTeX 與 PowerPoint 在文件撰寫上的角色。
語言特性
Quarkdown 以 .qmd 副檔名的文件格式，在標準 Markdown 之上提供：
- 函式呼叫：以
.functionname {arg1} {arg2}語法呼叫內建或自訂函式，如.sum {1} {2}在渲染時計算為3。 - 變數與迭代：以
.var name {value}宣告變數，.foreach {list} { item -> ... }迴圈展開。 - 自訂函式：以
.function functionname param1:type { body }定義可複用的文件元件。 - 數學：以
$...$/$$...$$嵌入 LaTeX 數學（透過 KaTeX 渲染）。 - 佈局原語：
.row、.column、.grid等容器，以及.slide/.focus演示文稿特有元素。
輸出目標
單一 .qmd 原始檔可編譯為：HTML（含互動動畫）、PDF（透過 headless Chrome 的 print-to-PDF），以及以 reveal.js 為基礎的可分頁演示文稿。
與既有方案的比較
相對於 Pandoc（廣泛格式轉換，但無腳本執行）、R Markdown/Quarto（以 R/Python 腳本驅動，依賴語言運行時），Quarkdown 以其自有的小型腳本語言運行，無需安裝 R 或 Python。HN 討論中主要與 Typst（類 Rust 語法的現代排版語言）比較：Typst 在數學與印刷排版有更完整的支援，Quarkdown 則更接近 Markdown 的書寫體驗。
原始來源：Quarkdown 官網、HN 討論
macOS 27 網路棧變更：新 API 取向與對 TCP/UDP 應用的影響
eclecticlight.co · 2026-04-23
Howard Oakley 在 eclecticlight.co 整理了 macOS 27（預計 2026 年 WWDC 發布）中已知的網路子系統變更，在 HN 引發 181 點、156 則留言的熱烈討論，聚焦在對開發者 API 的影響。
主要變更方向
macOS 27 繼續推進 Apple 自 macOS 12 起加速的「Network Framework 優先」策略：逐步棄用基於 POSIX socket（socket()/bind()/connect()）的直接呼叫，引導開發者轉向 Network.framework（NWConnection、NWListener、NWPathMonitor）。Network.framework 在系統層整合 TLS 1.3、QUIC 與 HTTP/3 支援，並對多路徑 TCP（MPTCP）有原生支援。
對既有程式碼的影響
使用 BSD socket 的 C/C++ 函式庫在 macOS 27 上預計繼續運作（向後相容承諾），但部分 setsockopt() 的進階選項（如 TCP_NODELAY 的某些語義、自訂 DSCP 標記）在 Network.framework 介面下的行為有所差異，可能影響低延遲應用（遊戲、音訊流）的調優。HN 討論中多位嵌入式網路函式庫維護者（curl、libuv 相關開發者）留言討論適配成本。
QUIC 與 HTTP/3 的系統整合
macOS 27 預計進一步將 QUIC 整合至系統 URL loading 基礎設施，使 URLSession（Swift/Obj-C）自動使用 HTTP/3，對使用系統 URL loading 的 iOS/macOS 應用無需修改即可受益，但繞過此層直接管理 socket 的應用需自行評估相容性。
原始來源：eclecticlight.co — Networking changes coming in macOS 27