热门标签：
Mac 多显示器 显示器扩展 requests patch 并发 Alpine Linux BSD Linux 电动汽车 全部标签

LLM辅助下的DSL设计新方向：模糊与形式的桥梁

2025-06-17

作者探索了大型语言模型（LLM）与领域特定语言（DSL）结合的新方向。作者日常使用LLM编写脚本，发现LLM擅长生成“粘合代码”，即根据自然语言描述生成代码框架，而复杂的逻辑仍需手动编写。这引发了作者对DSL设计的思考：如何将这种LLM辅助的编程流程集成到DSL中？如何弥合正式代码与非正式自然语言描述之间的差距？作者设想DSL能自动生成自然语言规范，并与非正式文本无缝集成。

阅读更多
(kirancodes.me)
开发

数学家如何证明：Lean Blueprints 可视化项目规划

2025-05-11

Lean Blueprints 是一种用于规划精益项目的工具，它借鉴了数学家用于形式化证明过程的蓝图方法。该工具使用图来表示证明过程中的不同步骤，节点代表定义、引理和定理，颜色表示状态（绿色为已证明，蓝色为已陈述但未证明，黑色为未写）。通过追踪Lean项目（例如Terrence Tao对PFR猜想的形式化）的版本控制，我们可以可视化地观察到证明过程的演变，从而洞察数学家如何进行证明，并为开发辅助数学家进行证明的工具提供数据。

阅读更多
(kirancodes.me)
开发 Lean Blueprints