私はConcrete v2仕様に取り組んでいます。最初のバージョンにはすでに動作するコードがあり、実装を通じて多くを学びました。今はZig、Austral、Lean/Coqから来た新しい興味深い機能を追加しました。 私は最初から形式的検証を中心にしたシステム言語を設計しており、興味深い特徴も含まれています。 特徴: - リーン4で形式化されたカーネル - リニアタイプ(オーストラルスタイル、ラストのアフィンではない) - 生涯注釈なしの借入 - 効果追跡機能 - アロケータを能力として渡す(Zigスタイル) - デフォルトで純粋 - !不純関数(Rocより) 作曲方法: 線形型は基盤です。すべての値はちょうど一度消費されます。漏れもなければ、二重無料も、自由な後も使わなかった。GCなしのメモリ安全。アフィンタイプよりも冗長ですが、より具体的で明確です。 借用することで線形性が使えるようになります。値を消費せずに一時的に参照してください。Rustの生涯注釈の代わりにレキシカル領域を使うこと。コンパイラはRustで書かされる内容を推測します。 機能は効果を追跡します。ファイルを読み取る関数がそれを宣言します。割り当てを行う関数が宣言します。宣言がなければ効果はない、保証される。grep with(Network)はネットワークに関わるすべての関数を見つけます。 アロケータを能力として使うことで、割り当てが可視化されます。with(Alloc)なしのコードはヒープに一切触れないことが証明されています。どの割り当て者がどのコードパスにサービスを提供するかをあなたがコントロールします。アリーナ、プール、スタックの割り当て、すべて明示的です。 Pureはデフォルトで通常のモデルを逆にします。効果には宣言が必要です。一般的な場合(純粋計算)は注釈を必要としません。 リーンの核がそれらをまとめています。コンパイラがあなたのプログラムが安全だと言うとき、その主張は証拠によって裏付けられています。