AIが書いたコードを、より安全にするために作っている言語。

01 — なぜ作っているか

エージェントが書いたものを、もう全部は読めません。

今は、自分のコードの多くをAIエージェントが書いています。近いうちに多くの人がそうなると思いますし、レビューはその量に追いつきません。

だから、安全性のより多くの部分がコンパイラから出てきて、誰かが丁寧に読むことに頼る部分が減る言語が欲しかった。自分で書いていないコードでも、頼れるものが欲しかったのです。

AIに書いてほしい言語はRustだと思います。でも正直、自分はRustが得意ではなく、所有権には最後まで慣れませんでした。Almideは、あの種類の安全性を保ったまま、人にもエージェントにも所有権の部分を書かせない、という試みです。

静的型付きで、ネイティブコードへはRustを経由してコンパイルし、WebAssemblyは直接出力します。Option と Result、網羅的なパターンマッチ、明示的なエフェクト宣言があります。

02 — 間違えようがない

所有権は書きません。コンパイラが推論します。

type Order = { id: Int, items: List[String], total: Int }

fn large(orders: List[Order]) -> List[Order] =
  orders |> list.filter((o) => o.total > 500)

fn main() -> Unit = {
  let orders: List[Order] = [
    { id: 1, items: ["pen", "ink"], total: 260 },
    { id: 2, items: ["desk"], total: 900 },
  ]
  let big = large(orders)
  println("${list.len(orders)} orders, ${list.len(big)} large")
  for o in orders {
    println("${o.id}: ${list.join(o.items, ", ")}")
  }
}

$ almide run orders.almd --target wasm
2 orders, 1 large
1: pen, ink
2: desk

orders は large に渡したあと、ループでもう一度使っています。ソースのどこにも、ムーブ・借用・コピーのどれなのかは書かれていません。ライフタイムも free もありません。

ヒープ上の値がどこで作られ、共有され、消費されるかは、コンパイラがPerceus式の推論で割り出します。2つのターゲットは、その結果を別々のやり方で実行します。ネイティブの出力はRustで、解放はRust自身のdropが行います。Wasmは参照カウントを使います。

03 — いちばん大事にしている部分

コンパイラに、自分の採点はさせません。

自分は、自分のコンパイラを信用していません。AIエージェントと一緒に作ったものを、どうして信用できるでしょうか。

Wasmをビルドするたびに、コンパイラは自分がやったことの証拠を書き出さなければなりません。値を共有したり解放したりしたすべての場所、検査したすべての配列の添字です。その証拠を別のプログラムが読みます。つじつまが合わなければ、出力ファイルはできません。

拒否は、あなたのバグではありません。コンパイラのバグです。ビルドはそう報告します。

error[certificate-rejected]: app.almd: almide-verify judged this build's
certificate and did not accept it (exit 1)
  app.wasm was not written: the build's own certificate does not hold,
  which is a compiler bug — please report it

一部を省略しています。1行目のあとに、検証器自身の報告が続きます。

04 — TRUST SPINE

検査器にもバグはありえます。だから4つあります。

検査器が1つだけなら、信頼の置き場所が移るだけです。この4つは作り方がそれぞれ違うので、同じ間違いがすべてに入り込むことは起きにくくなっています。検査される証拠とあわせて、このプロジェクトではこれを Trust Spine（信頼の背骨）と呼んでいます。

CIでは、Proofcore・Proofcast・Buildgate の3つが、テスト用のすべてのプログラムのすべての証拠について、同じ判定を出さなければなりません。この仕組みでの拒否は、自分のコンパイラの実際のミスコンパイルをすでに1つ捕まえています。

証明は、リポジトリにある46個のRocqファイルです。約21,700行で、定理と補題が654個あります。対象は検査器とそのモデルで、コンパイラではありません。

証拠は何についてのものか

証拠には種類があり、性質ごとに1つずつあります。種類ごとに規則が決まっていて、4つの検査器が当てはめるのはその規則です。

これらは、証拠が覆っているコードについて成り立ちます。Byteanchor は bounds・init・fields の証拠を実際のバイト列と突き合わせ、記録された参照カウントの操作を、ファイルの中の呼び出しと照らし合わせます。命令に結びつけられなかった操作は、黙って通すのではなく、「位置を特定できなかったもの」として数えます。

05 — コードが間違っていたとき

エラーが、何を直せばいいかを教えます。

エージェントは間違えます。大事なのは、そのあと何が起きるかです。ほかの言語を学んだエージェントは items.length と書きます。

error[E013]: no field 'length' on list
  --> app.almd:3:14
  in field access .length
  here: println("${items.length}")
  hint: Almide values have no fields — use the `list` stdlib module.
  try: (machine-applicable — `almide fix` applies it)
      list.len(items)

$ almide fix app.almd
  Applied 1 machine-applicable fix-it(s) from diagnostics: E013 at line 3

これは機械的に直せるので、ツールが適用します。関数名の打ち間違いは違います。

error[E002]: undefined function 'string.lenn'
  hint: Did you mean `string.len`?

$ almide fix app.almd
1 diagnostic(s) have `try:` snippets that need manual application:
  [E002] app.almd:3:14  undefined function 'string.lenn' (maybe-incorrect)

0.69.0 のコンパイラ出力です。一部を省略しています。

こちらは、書き手が何を意図したかについての推測です。だから候補のままにします。機械的な修復と、意図についての判断との境目を、ツールの中で見えるようにしておきたいと考えています。

06 — 出荷されない間違い

場合分けの書き忘れは、コンパイルエラーです。失敗の無視も同じです。

エージェントの編集でいちばんよく見る間違いは、型にバリアントを足して、それを処理すべき場所を1つ見落とすことです。

type Shape =
  | Circle(Float)
  | Rect(Float, Float)
  | Triangle(Float, Float)      // 追加した

fn area(s: Shape) -> Float = match s {
  Circle(r) => 3.14159 * r * r,
  Rect(w, h) => w * h,
}                               // 直し忘れた

error[E010]: non-exhaustive match: missing Triangle(_, _)
  --> shape.almd:6:36
  hint: add arms for Triangle(_, _):
  Triangle(arg1, arg2) => _

失敗の扱いも同じです。失敗しうる呼び出しは Result を返し、それをどうするかを書かなければなりません。黙って捨てるのは、警告ではなくエラーです。

effect fn load(path: String) -> String = {
  let text = fs.read_text(path)     // 失敗しうるのに、どこにもそう書いていない
  text
}

error[E041]: implicit propagation of this binding's value was removed —
this value is a Result
  --> load.almd:4:14
  hint: Write `expr!` to propagate, or consume the Result as a value
  (`??`, `?`, match ok/err).

0.69.0 のコンパイラ出力です。一部を省略しています。

直すのは1文字です：fs.read_text(path)!。大事なのは、書き手が決めなければならなかったこと、そしてその決定がソースに見える形で残ることです。

07 — 1つのソース、2つのターゲット

同じソースからネイティブと WebAssembly を作り、同じ出力を求めます。

ネイティブのビルドはRustを経由します。WebAssemblyは、LLVMを挟まずにコンパイラが直接出力します。hello world は 325 バイトの .wasm ファイルになります。

バックエンドが2つあれば、食い違うことがあります。だから、外から観測できる約束はすべて「契約」として書き出してあります。今は454個あり、一つ一つが実行できる証拠に結びついています。CIは1,055本のプログラムを両方のターゲットで実行し、標準出力・標準エラー・終了コードを比べます。3つ目の実行系として、コード生成の前の段階でプログラムを実行するインタプリタも判定に加わります。

この比較は、文書に書かれた条件のもとで成り立ちます。乱数、時計、プラットフォームの細部には、それぞれ範囲を区切った契約があります。インタプリタは、実行できない17本については判定を棄権します。

08 — ほかに入っているもの

デモではなく、ひとそろいの言語です。

09 — まだできていないこと

完成していません。そこははっきり言っておきます。

• コンパイラ全体は証明されていません。証明が覆っているのは、検査器とそのモデルです。
• ネイティブのビルドは検証器を実行しません。認証つきのレンダラを通り、テスト用のプログラムは今はすべてそこを通ります。ただし、証拠を判定するのはプロジェクトの検証の中で、手元のビルドのときではありません。レンダラが扱えないプログラムは、今も通常のコード生成に戻ります。
• 手元のマシンで動くのは、4つの検査器のうち1つだけです。ほかの3つは、CIでテスト用のプログラムに対して動きます。検証器が入っていなければ、Wasmのビルドは検査なしで通ります。
• 証拠が部分的な場合があります。プログラムの一部しか覆っていない証明書も通します。component 出力はこの方法では検査されません。
• 記録された操作のすべてが、命令に結びつけられているわけではありません。Byteanchor は、位置を特定できなかったものを数として報告します。その数は、どこでもゼロというわけではありません。
• すべての検査を通ったプログラムでも、計算結果が間違っていることはあります。この仕組みは、ロジックが正しいかどうかを見るものではありません。
• エージェントがRustやTypeScriptよりAlmideをうまく書ける、とは示せていません。最初の計測は、強いモデルではどの言語でもほぼ100%になり、何も分かりませんでした。
• 1.0 より前です。既知のバグがあり、これからも変わります。

何が証明済みで、何が信頼に置かれているだけなのかの全体は、リポジトリにあります：proven vs trusted（英語）。

10 — どう作ったか

AIエージェントと一緒に作りました。それが出発点です。

コンパイラはRustで書かれていて、書くのにAIエージェントをたくさん使いました。先にそう言っておきます。そうやって作られたものは見たくない、という人もいるはずで、それはもっともだと思うからです。

ただ、このプロジェクトがこういう形をしている理由も、そこにあります。エージェントがコンパイラを書くのなら、自分が読んだことを根拠に保証することはできません。だからコンパイラは証拠を出さなければならず、別の何かがその証拠を検査しなければならない。これは、エージェントを使う人すべてが、自分のコードについてこれから抱える問題と同じです。Almideは、その問題に公開の場で取り組んでいるものです。

11 — 試す

どこで壊れるか、見てください。

Playground はブラウザで動き、インストールは要りません。macOS か Linux にコンパイラと検証器を入れるには：

curl --proto '=https' --tlsv1.2 -fsSL \
  https://raw.githubusercontent.com/almide/almide/main/tools/install.sh | sh

インストーラは、リリースの署名を確かめるために GitHub CLI（gh）を必要とします。Windows とソースからのビルドは README にあります。