OCamlPro创建于2011年，旨在倡导业界普遍采用OCaml语言和正式方法。2021是一个非常特殊的一年，因为我们庆祝我们的第十周年！在组建一支由高技能工程师组成的团队时，我们像往常一样通过我们的专业领域、编程语言设计、编译和分析、高级开发人员工具、正式方法、区块链和高价值软件原型设计进行导航。
在这篇文章中，如每年（见OcLLPRO去年2020和第39篇文章），我们回顾我们在2021年间在许多不同领域所做的一些工作。
一如既往，我们衷心感谢所有客户、合作伙伴和朋友在这特殊的一年里给予我们的支持和合作！
没有员工，公司就一无是处。今年，我们很高兴地欢迎了大量新来者：
Hichem Rami Ait El Hara最近完成了他的硕士学位#39；她拥有计算机科学学位。在OCamlPro实习期间，他为Alt Ergo开发了一个fuzzer，之后他加入了OCamlPro，致力于Alt Ergo和智能合同的验证。他将很快开始攻读SMT解决的博士学位。
Nicolas Berthier拥有资源受限系统同步编程博士学位。凭借多年的模型检查、抽象解释和软件分析经验，他加入OCamlPro从事编程语言编译和分析工作。
Julien Blond是一名高级OCaml开发人员，在安全软件的正式验证方面拥有丰富的经验。他以项目经理和Coq专家的身份加入OCamlPro。
Keryan Didier以R&；D工程师。他拥有皮埃尔·玛丽·居里大学（University Pierre et Marie Curie）的博士学位，在此期间，他开发了一种用于硬实时应用程序的自动化实现方法。此前，他曾在巴黎狄德罗大学学习函数式编程和语言设计。Keryan参与了MLang项目以及OCamlPro和#39内的flambda2项目；我的编辑团队。
穆罕默德·赫努夫最近完成了他的硕士学位#39；她拥有计算机科学学位。在OCamlPro实习并在OCaml文档中心工作后，他加入了OCamlPro，并继续在文档中心和其他OCaml应用程序上工作。
达里奥·平托是巴黎计算机科学学院的学生。他与OCamlPro签订了为期两年的勤工俭学合同。
Artemiy Rozovyk最近完成了他的硕士学位#39；她拥有计算机科学学位。他加入OCamlPro，致力于EverScale和Avalanche区块链应用程序的开发。
M语言是一种非常古老的编程语言，由法国税务局开发，用于计算所得税。最近，Denis Merigux和Raphael Monat用OCaml为M语言实现了一个新的编译器。与以前的编译器相比，这种新编译器表现出更好的性能、更清晰的语义，并实现了更高的可维护性。OCamlPro现在正致力于加强这个新的编译器，将其投入生产，并最终计算出3000多万个法国家庭的税收。
COBOL语言诞生于60多年前，就计算机中运行的行数而言，据说它仍然是世界上使用最多的语言，尽管许多人预测它将在21世纪末消失。它有300多个保留关键字，也是解析和分析最复杂的语言之一。它'；这还不足以吓唬OCamlPro的开发人员：在帮助法国最大的COBOL用户之一将其程序翻译成GNUCobol开源编译器的同时，OCamlPro构建了强大的COBOL和大型机专业知识，并开发了一个强大的COBOL解析器，这将帮助我们为COBOL开发人员带来现代开发工具。
Geneweb是迄今为止管理和共享家谱数据最强大的软件之一。它是20多年前用OCaml编写的，包含一个web服务器和复杂的算法来计算家谱信息。家谱网是家谱学领域的领先公司之一，它用来存储80多万棵家谱和70多亿个祖先的名字。OCamlPro目前正在与Geneanet合作，以改进Geneweb，并使其能够扩展到更大的数据集。
Mosaic平台为生态毒理学领域的研究人员、工业参与者和监管机构提供了一种简单的方法来运行各种统计分析。用户只需在web界面上输入一些数据，然后在服务器上运行计算并显示结果。该平台完全用OCaml编写，并负责调用用R编写的数学模型。OCamlPro使项目现代化，以便于维护和新贡献。在这个过程中，我们发现了新R版本引入的bug（没有任何警告）。然后我们开发了一个新的数据输入接口，它'；它类似于电子表格，比编写原始CSV方便得多。在这项工作中，我们有机会对其他一些OCaml包（如leveldb）做出贡献，或者编写新的OCaml包（如agrid）。
OCamlPro很自豪能够参与Flambda2，这是一个雄心勃勃的OCaml优化编译器项目，由我们的长期合作伙伴和客户Jane Street的Mark Shinwell发起。Flambda专注于降低抽象的运行时成本，并尽可能多地删除短期分配。Jane Street已经启动了flambda2的大规模测试，在我们这方面，我们已经记录了一些关键算法的设计。2021，弗兰巴达队和Keryan的队伍越来越大。随着大量的修复和改进，这将使我们能够在未来几个月发布Flambda2！
在其他OCAML编译器新闻中，2021将期待已久的多核分支合并到官方开发分支中。这要感谢许多人的出色工作，包括我们自己的达米恩·多利格斯。但这还远未结束，我们'；我们期待着进一步为编译器做出贡献（修复bug，重新启用对所有平台的支持），并在我们自己的程序中利用这些功能。
Opam是基于OCaml源代码的包管理器。第一个规范草案是在2012年初编写的，后来成为OCaml的官方包管理器——尽管它可能用于其他语言和项目，因为Opam是语言不可知的！如果您需要轻松安装、升级和管理编译器、工具和库，Opam是为您设计的。它支持多个同时安装的编译器、灵活的包约束和Git友好的开发工作流。
Opam开发和维护是OCamlPro与Raja&；Louis和OCamlLabs，以及David Allsopp&；凯特·德普莱克斯。
我们在OPAM上的2021项工作最终导致了期待已久的OPAM 2.1、三版本的OPAM 2和两个版本的OPAM 2.1的最终发布。
切换不变量，替换"；基本包"；在opam 2.0中，允许更轻松地升级编译器
CLI版本控制，允许现在对opam进行更干净的弃用，并在未来改进语义，同时不破坏向后兼容性
在2021，我们还准备了即将发布的OPAM 2.2版本的alpha版本。它将更好地处理Windows生态系统、集成SoftwareHeritage归档回退、更好的用户界面交互、递归固定项目、获取优化等。
我们还积极维护Learn ocaml。最初设计为OCamlMOOC平台的工具现在是OcAML全球教师手中的工具，由OAML基金会管理和资助。
这项工作包括为OCaml 4.12提供一个逾期已久的端口；生成可移植可执行文件（通过CI自动生成），以便更轻松地部署和使用命令行客户端；以及许多生活质量和可用性的改进，这些改进来自于与许多老师的双向对话。
在一个相关的问题上，我们还修改了在线OCaml编辑器和顶级TryOCaml，改进了它的设计，并添加了代码片段共享等功能。我们高兴地看到，在这些困难时期，这些工具对教师和学生都很有用，并期待着进一步改进。
作为OCaml的最大用户之一，OCamlPro旨在通过开发大量开源工具来促进OCaml的日常使用。
我们在OcAML生态系统2021的主要贡献之一可能是OCSL文档中心在DOCS。ocaml。赞成的意见。
OCaml文档中心是一个为2000多个OPAM软件包提供文档的网站，其中当然最流行的是软件包间的文档链接！该网站还包含所有这些软件包的可浏览资源，以及一个搜索引擎，用于发现有用的OCaml函数、模块、类型和类。
所有这些文档都是使用我们的定制工具Digodoc生成的。尽管它'；在一个特定的区域，我们还一直在维护Drom、我们的沙丘层和Opamt，这是我们最近大多数项目使用的。
去年，人们期待已久的SoftwareHeritage和OCamlPro之间的合作也得以实现。
多亏了艾尔弗雷德·P·斯隆基金会的资助，OCamlPro已经能够与我们的软件遗产合作伙伴合作，并通过存档3516个OPAM包来进一步扩大他们的巨大努力的覆盖面。实际上，这种开源协作的主要好处是：
在软件遗产架构中增加了几个模块，允许对所述opam包进行归档；
如果opam上的给定软件包不再可用，则实施可能的软件遗产回退；
在软件最终被联合国教科文组织确认为世界遗产的一部分后不久，我们很高兴成为这一伟大而有意义的倡议的一部分。我们可以感觉到，在我们的互动过程中，以及在工作完成后的很长一段时间里，真正的激情依然存在。
OCamlPro开发并维护Alt Ergo，这是一种基于可满足性模理论（SMT）的数学公式自动求解器，用于程序验证。ALT ErGo最初是在巴黎萨克莱大学的VARS团队中创建的。
在2021，我们继续专注于我们的求解器的可维护性。我们分别在1月和7月发布了版本2.4.0和2.4.1，其中2.4.1包含错误修复和一些性能改进。
为了增加我们的测试覆盖率，我们检测了Alt Ergo，以便使用afl fuzz运行它。虽然这是一个概念证明，但尚未被纳入Alt ergo'；在不断的集成中，它已经帮助我们发现了一些错误，比如这个。
我们感谢Alt Ergo用户俱乐部、Adacore、CEA List、MERCE（三菱电气欧洲研发中心）、Thalès和Trust In Soft的合作伙伴对我们的信任。他们的支持使我们能够维护我们的工具。
该俱乐部于2019推出，第三届阿尔戈用户俱乐部年会于2021年4月初举行。我们的年会是审查每个合作伙伴关于Alt Ergo需求的完美场所。今年，我们有幸与合作伙伴讨论了未来Alt Ergo功能和增强的路线图。如果您想参加我们的下一次会议（即将召开），请联系我们！
最后，我们将能够把我们在2020年所做的一些工作合并到Alt Ergo的主要分支中。感谢我们的合作伙伴MERCE（三菱电气欧洲研发中心），我们致力于SMT车型的开发。Alt Ergo现在（部分）能够以smt-lib2格式输出模型。由于来自巴黎SACLY大学的WHY3团队，我们希望这项工作将在WHY3平台上提供，以帮助用户在他们的程序验证工作中。
这项工作的部分资金来自FUI R&；D项目LCHIP、MERCE、Adacore和Alt Ergo用户俱乐部的支持。
Dolmen是一个功能强大的库，为自动推理中使用的多种语言提供灵活的解析器和类型检查器。
正在进行的将Dolmen库用作Alt Ergo前端的工作已经取得了相当大的进展，dolemn已经扩展到支持Alt Ergo'；在这个公共关系中，以及在Alt Ergo'；s端添加dolmen作为前端，可以在本PR中选择。一旦这些被合并，Alt Ergo将能够读取新语言的输入问题，例如TPTP！
几个月前，我们发表了一系列帖子：假人验证：SMT和感应。这些帖子介绍并讨论了SMT解算器、归纳和不变强化的概念。他们依赖mikino，这是我们编写的一个简单软件，可以分析简单的过渡系统，并执行基于SMT的归纳检查（以及BMC，即错误查找）。我们在《铁锈》一书中以可读性和人体工程学为出发点编写了mikino：mikino展示了编写基于SMT的模型检查器执行归纳的基础知识。这些帖子非常实用，并且利用了米基诺'；s的高质量输出讨论归纳和不变强化，读者可以运行和编辑自己的例子。
在2021，我们最终使用了TLA+语言及其相关的TLC验证引擎在几个完全无关的项目中。TLC是一个了不起的工具，但它不适合处理包含许多模块（文件）、回归测试等的TLA+项目。特别是，TLA+不是类型化语言。这意味着TLA+代码往往会有许多检查（动态断言）来检查数量是否具有预期的类型。这很好，虽然在某种程度上有点乏味，但随着代码变大，TLC进行的分析可能会变得非常非常昂贵。最终，保持断言类型检查一切是不合理的，因为它有助于TLC'；他的分析爆炸了。
作为TLA+/TLC用户，我们目前正在开发管理TLA+项目的matla。玛特拉以铁锈书写，深受铁锈生态系统的启发，尤其是货物。Matla尚未公开发布，因为我们正在等待早期用户的更多反馈。不过，我们确实在内部使用它，因为它的各种功能使我们的TLA+项目更加简单：
提供一个带有"的Matla模块；调试断言"；助手：这些断言在调试模式下是活动的，这是运行matla run时的默认模式。通过——释放给马特拉'；但是，s运行模式会编译掉所有调试断言；这允许在调试时对所有内容进行类型检查，同时确保发布运行不会支付这些检查的费用；
处理集成测试：matla项目有一个测试目录，用户可以在其中编写测试（带有.TLA和.cfg文件的TLA文件），并指定测试是成功还是失败（以及如何进行）；
理解并转化TLC'；s的输出，以改善用户反馈，尤其是当TLC产生错误时（还不够好，这是我们尚未发布的原因）；matla还解析和美化TLC'；s通过格式化值、格式化状态（值的聚合）和使用ASCII艺术以图形方式呈现状态跟踪来反例跟踪。
目前的大流行无疑正在影响我们的专业培训活动。尽管如此，我们还是有机会在夏季与ONERA的应用研究人员一起举办了一次锈病培训课程。该课程为期一周（每天约七个小时），是我们第一次完全远程培训课程。我们仍然认为现场培训（如果可能）更好，全远程提供了一些灵活性（例如，将培训分散在几周内），我们与ONERA的经验表明，它可以在实践中使用正确的技术。有趣的是，事实证明，远程教学在某些方面实际上效果更好：例如，动手练习和项目受益于屏幕共享。与一名参与者讨论代码是通过屏幕共享完成的，这意味着如果所有参与者愿意，他们都可以跟随。
长话短说，完全远程培训是我们现在有信心向客户提出的一种灵活的现场培训替代方案。
我们参加了一场旨在为TON VM汇编程序编写（编译器）高级规范的竞赛，特别是它的指令及其编译方式。这场竞赛是向TON虚拟机应用正式方法，尤其是正式验证迈出的第一步。我们很高兴地报告，我们在这方面取得了第一名，并期待着未来的竞赛进一步推动Everscale区块链中的正式方法。
2019-2020年，我们与Origin实验室合作，集中精力开发区块链，向Dune Network生态系统添加新的编程语言。你可以阅读更多关于沙丘的爱和坚固。
2020年底，很明显，高吞吐量正在成为实际应用中采用区块链的主要要求，Dune Network背后基于Tezos的技术无法与Solana或Avalanche等高性能区块链竞争。根据这一观察，沙丘网络社区决定在2021年初与弗里顿社区合并。最初由Telegram开发的TON项目因法律威胁而停止，但另一家公司TONLabs以FreeTON的名义从其开源代码重新启动了该项目，区块链于2020年中期启动。FreeTON现在更名为EverScale，是当今世界上速度最快的区块链，在一个开放的网络上，在几天内每秒大约有55000笔交易。
EverScale采用了一种非常独特的社区驱动开发流程：竞赛由主题次级政府（subgov）组织，以改善生态系统，参赛者赢得代币价格，以奖励他们的高质量工作。在2021期间，OCamlPro参与了其中的几个分治，既有陪审团，也有正式的方法SuGOV和开发者体验SuGOV，以及一个争夺智能合同开发的多个价格的竞争者（ZKSNARACK用例，拍卖和经常性支付），对多个智能合约的审计（TrueNFT审计、智能多数投票审计和一个DEX审计），以及节点（汇编程序模块）中一些生锈组件的规范。
EverScale生态系统中的这项工作让我们有机会开发一些有趣的OCaml贡献：
我们改进了ocaml solidity解析器，以支持解析EverScale合同所需的solidity语言的所有扩展；
我们开发了一个名为ft的命令行钱包，帮助开发者轻松部署合同并与之交互；
我们在Dune Network和EverScale之间建立了一座桥梁，将DUN代币交换为EVER代币。
我们最近在EverScale区块链上的工作旨在开发Why3框架，以正式验证EverScale Solidity合同。与此同时，我们已经参与了几个大型智能合同项目的规范，我们计划在这些项目正式验证开始后立即在实践中使用该框架。
我们希望能够将这项工作扩展到以太坊、雪崩和许多其他区块链上的基于EVM的实体合同。与其他直接在EVM字节码上工作的框架相比，这项工作直接集中在Solidity语言上，应该使验证更高级别，因此更直接。
我们出席了巴黎新版开源体验！我们的展位欢迎参观者讨论定制的软件解决方案。Fabrice有机会就FreeTON（现在的EverScale）做了一个演示（观看视频），这是他正在研究的高速区块链。我们很高兴见到开源社区。此外，艾美莉
......