C*：C言語に証明を統合し、プログラマ自身によるリアルタイム検証を可能にする

私はしばらくこの馬に乗っています。Ada/SPARKを学ぶことに決めました。Ada 2022は新しいSPARK 2014アップデートを供給し始めるでしょう。ええ、両方とも冗長で、そういうのが好きでなく、Pascal風の構文が好きでないなら。信じてください、私はAPL/J/k/uiua/BQNやForth、ASMが好きです。私は通常、構文にはこだわりません。プログラミング言語とエコシステム（多くの人が考える以上に重要）があなたのニーズを満たす限り。私は2018年にRustを試し、2023年にも再度試しましたが、非常に複雑で、まあ、構文は好きではありませんでした。MLやHaskellに似た構文の方が好みでした。Zigは良さそうでしたが、ユースケースが異なり、新しすぎました。結局、Ada/SPARKは何十年もの間、巨大で高信頼性・高安全性のアプリケーションで使われてきました。Rustは彼らの愛の一部を得つつあり、その逆も然りです。AdaCoreは検証済みのRustコンパイラを作成しましたが、実際の製品（Blacktailホイスト）を開発中であり、高安全性と標準認証を達成するには、ツールセットと保証、監査と受け入れの容易さが必要です。航空宇宙、防衛、鉄道、自動車を考えてください。私は1977年にプログラミングを始めたので、ASM/Cにはいつも心の中に場所があります。F#、F*、MSのLOWを試しましたが、それらは良いですが、Rustと同様に、Ada/SPARKのような実際の遺産がありません。私はShenを使って、ソフトウェアの安全性がそれほど重要でない分野の形式的に検証されたモデルを書いていますが、それは新鮮だと感じます。しかし、私の本業は、Rustがより成熟するまでAda/SPARKに集中することです。