りよ

WireCat はデカルト圏に対応するグラフィカルな記法でプログラムを記述できる Haskell の GHC プラグイン👀 Arrow と異なり関数の埋め込みをできなくすることで中身の静的解析が可能になり、依存グラフの図を出力したりもできる。ノードは拡張可能レコードで柔軟に管理 guaraqe.com/posts/2026-05-…

プログラムを滑らかに変形したい…

微分可能プログラミングとかソフトウェア2.0みたいなの昔聞いたけどちょっと違うか

今後プログラミングにパラダイムシフトがあるとしたら、柔らかい言語、みたいな概念が出てきたら面白いなと思っている ベクトル空間みたいになっていて滑らかに変化させることが可能で、その軌跡を辿ることでマイグレーションとかも出来る　形式検証はある範囲内に入っているかを検証することになる

Linear Haskell を使ってデッドロックを起こさないことを保証するライブラリ linear-locks 楽観ロックのSTMと異なり静的に保証することができロックを取得しながらIOを伴う処理を行うこともできる github.com/dcastro/linear…

Haskellのエフェクトライブラリですが6月に集中開発してリリースして記事とスライドを作る予定

みんなトークン効率の話しかしない　そもそも設計でオーダーレベルでコード行数変わるんだから設計の話をするべきである

予想だっけ、忘れたけどなんか性質についての形式文

たしかVerus言語でコーディングエージェントやる論文だかで、生成した予想候補に最初にPBTにかけて安価に弾くやつやってたなあ

New blog post: On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications. proofsandintuitions.net/2026/05/18/pro… The gist: randomised testing can validate formal specs. It's very cheap and powerful: we found bugs in specs of VERINA and CLEVER benchmarks.

提供側でプラグインシステム作るなら実行隔離された wasm extension 採用しろと言ってる。 ホストと同じ実行権限与えるのはそもそもおかしい。

@miura1729 定量的な情報をモナドに持たせるとできるみたい dl.acm.org/doi/10.1145/34…

初めて見た　なんだこれは

これ (CoT) ちょうど昨晩見てたんだけど何が起こっているのかがまるでわからなかった ちゃんと Monad インスタンスの実装を見るべきかもしれない

newtype Co w a = Co { runCo :: forall r. w (a -> r) -> r } を使ってコモナドから対応するモナドの実装を作れるのすごい👀 それを Codensity と右カン拡張を使って導出できるのも面白い comonad.com/reader/2011/mo…

@t3tra_x ご存知でしたね、すいません…！独自実装してるの凄い

@ymdfield ありがとうございます！ まさにAlphaProofの類の研究は調べて知ったのですが LLMに既存の定理証明支援系を書かせるのは中々骨が折れますしLLM自身の能力を超えられず頭打ちになってしまうかなーと思いまして ここでは独自の小さなカーネルへの翻訳層をNLPによるエンコーダとして実装しています！

(やりたいことは伝われ)

@t3tra_x もっともこれらは形式証明を出力するだけであって、推論過程（chain-of-thought内）も形式化するのは見たことないですが、おそらくできることは近いはず…

@t3tra_x 唐突にすみません、ご存知でしたら申し訳ないのですが、LLMとLean等を組み合わせてハルシネーションを防ぐのは自動定理証明やAutoformalizationの文脈で最近よく論文が出ているので興味があれば調べてみてください（Seed-ProverやHerald translatorなど）

進化型多目的最適化の代表的な手法を比較した記事を書きました。 NSGA-II、SPEA-II、NSGA-III、HypE、MOEA/D について、環境選択の違い、パレートフロントの形状、目的数による性能差、計算時間を整理しています。 多目的最適化でどの手法を選ぶべきか考えるときの参考になればうれしいです。 nature-architects.com/blog/comparing…

Yulangという言語を作りました。Algebraic Effectsを入れているので非決定性計算、ジャンクション、変数などが自由に動きます。 playgroundは yulang.momota.pw で、リポジトリは github.com/momota1029/yul… です。記事は zenn.dev/momota1029/art… なので何かしら反応が欲しいです