从彭博社的Rocq定理证明器中提取已验证的C++代码。

从彭博社的Rocq定理证明器中提取已验证的C++代码。
Extracting verified C++ from the Rocq theorem prover at Bloomberg

原始链接: https://bloomberg.github.io/crane/

GitHub Wiki Issues Crane Rocq 的一种新型提取系统，旨在生成功能式、内存安全、线程安全、可读、有效、高性能和现代的 C++ 代码。在 GitHub 上查看最新版本：alpha 快速入门探索 Crane 的常见主题、指南和文档。入门安装 Crane，配置 Rocq，并运行你的第一次提取。设计原则 Crane C++ 提取策略背后的目标和权衡。示例浏览示例 Rocq 项目和提取的 C++ 代码。参考手册了解 Crane 的所有选项、提取规则和标志。 Crane 基础库我们从提取的代码中使用的 Rocq 类型、Monad 等库。路线图计划中的功能和即将到来的改进。论文 Crane 将 Rocq 安全地降级到 C++ (扩展摘要) Matthew Z. Weaver, Joomy Korkut. RocqPL 2026. © 2026 Bloomberg L.P. GitHub Wiki Issues

黑客新闻新 | 过去 | 评论 | 提问 | 展示 | 招聘 | 提交登录从彭博社的Rocq定理证明器中提取验证过的C++ (bloomberg.github.io) 3点由 clarus 2小时前 | 隐藏 | 过去 | 收藏 | 1评论 clarus 2小时前 [–] 一个新的从Rocq提取的系统，生成功能式风格、内存安全、线程安全、可读、有效、高性能和现代的C++。有趣的是，这可以集成到生产系统中，以快速正式验证关键组件，同时与彭博社现有的C++代码库完全兼容。回复指南 | 常见问题 | 列表 | API | 安全 | 法律 | 申请YC | 联系搜索：

Quick Start

Explore common topics, guides, and documentation for Crane.

Getting Started

Install Crane, configure Rocq, and run your first extraction.

Design Principles

The goals and tradeoffs behind Crane's C++ extraction strategy.

Examples

Browse example Rocq projects and extracted C++ code.

Reference Manual

Understand all Crane options, extraction rules, and flags.

Crane Base Library

Our Rocq library of types, monads, etc. used from extracted code.

Roadmap

Planned features and upcoming improvements.

Papers

Crane Lowers Rocq Safely into C++ (Extended Abstract) Matthew Z. Weaver, Joomy Korkut. RocqPL 2026.