Status: Design / RFC phase
Implemented compiler: No
Accepted RFCs: 0
Normative specification: Not yet established
証明できることと、信頼するしかないことを分けて見せる。
NEPLg3 は、前置記法、オフサイドルール、式指向を受け継ぎながら、依存型、精緻化型、契約、リソース検査、exact-first な数値系を一つの検証基盤へ統合するプログラミング言語である。
Rocq で仕様・参照コンパイラ・proof checker を定義し、WebAssembly を主要ターゲットとする。最終的には、NEPLg3 自身で記述した proof-producing compiler へ移行することを目指す。
Important
NEPLg3 は現在、仕様策定と実装計画の段階にある。コンパイラや Playground はまだ利用できない。この README に掲載する構文は候補であり、正式な RFC によって変更される可能性がある。
NEPLg3 が目指すのは、単に「型が強い言語」ではない。ソースコードから生成物まで、何が検査され、何が証明され、どこに仮定が残っているかを追跡できる言語処理系である。
- Proof と Runtime を分離する — 論理関数と実行時関数、Pure と Total、証明とリソースを混同しない
- 保証範囲を明示する — 型検査、VC、Wasm AST、バイナリ、ホスト環境を一括して「Verified」と呼ばない
- 正確な数を既定にする — 小数を暗黙に binary float へ丸めず、exact な値として扱う
- 所有権を意味論へ組み込む — move、borrow、drop、region を静的検査とコンパイラ検証の両方で扱う
- Web を第一級の実行環境にする — 参照コンパイラ自体を Wasm 化し、CLI と Web で同じ意味論を使う
- Self-host を信頼の近道にしない — 自己コンパイルだけで正しさを主張せず、独立した再検査経路を残す
NEPLg3 の最終構文は今後変更する予定だが、この README では当面、NEPLg2.1 の正規構文で表す。型注釈は %T expr、関数型は fn A B、副作用を持つ関数型は impure fn A B、関数宣言・関数リテラルの binder は \arg とする。前置呼び出し、if: / then: / else:、オフサイドルールもそのまま引き継ぐ。
次は examples/rpn.nepl の演算適用処理を題材に、NEPLg2.1 の関数宣言へ契約と証拠を加えた apply_op_values 候補例である。
#entry main
#indent 4
#target core
#import "core/math/i32/arith" as *
enum RpnOp:
Add
Sub
Mul
fn apply_op_values %fn RpnOp fn i32 fn i32 i32 \op\a\b:
contract:
ensures operator_semantics \result:
match op:
RpnOp::Add:
Eq i32 result add a b
RpnOp::Sub:
Eq i32 result sub a b
RpnOp::Mul:
Eq i32 result mul a b
body:
match op:
RpnOp::Add:
add a b
RpnOp::Sub:
sub a b
RpnOp::Mul:
mul a b
prove ensures operator_semantics:
by:
cases op
case Add:
simp
case Sub:
simp
case Mul:
simp
fn main %fn void i32 \void:
apply_op_values RpnOp::Add 1 2
contract:、body:、prove、by: は NEPLg3 で追加する候補であり、それ以外の外形は現在の NEPLg2.1 に合わせている。契約は VC を生成する仕様、prove は特定の claim に対応する evidence、by: は proof term を生成する式である。NEPLg3 の正式な差分は Syntax RFC で決定する。
prove ensures operator_semanticsには、verified WP／symbolic executionが生成したpath conditionとreturn valueを持つVCを渡す。通常のproofをevaluatorのconstructor構造へ依存させない。raw evaluation derivationの直接反転は、意味論自体を証明する低水準escape hatchに限定する。
少なくとも Proof Syntax RFC では、unit 型・unit 値の unit、ゼロ引数 marker の void、前置適用を維持する。()、expr : Type、\x => expr、f(a, b)への変更は前提にしない。
命題も型であり、その証明も通常の NEPL 式である。既存の期待型境界 %T expr を命題へそのまま拡張し、%P proof_expr を「proof_expr を命題 P の証明として検査する」と読む。
let add_zero %Eq Nat add n 0 n by:
simp
theorem と lemma の本体には proof term を置く。by: は tactic によって明示的な Core proof または certificate を生成する式であり、それ自体を kernel の authority にはしない。
theorem and_swap %Prop \P\Q %And P Q \h %And Q P:
by:
apply And::intro
case left:
exact And::right h
case right:
exact And::left h
theorem と lemma は既定で Total、Opaque、Erased とする。明示 proof term、match、再帰、induction principle の適用も通常式として書けるため、by: の使用は必須ではない。
solver が certificate を生成せず、結果を信頼する場合は oracle であることを構文上も明示する。
prove ensures external_claim:
oracle solver::z3
この evidence は TrustedOracle として依存関係へ記録し、--certified では拒否する。未完成の証明も hole として明示する。
prove ensures unfinished:
?unfinished_proof
hole は IDE で goal として表示できるが、release artifact と certified build では常に拒否する。
| 領域 | 方針 |
|---|---|
| 構文 | 当面は NEPLg2.1 と同じ prefix-oriented、off-side rule、expression-oriented な構文を用いる |
| 型 | Type / Prop、依存型、精緻化型、双方向型検査 |
| 関数 | effect と termination を独立して表現 |
| 検証 | contract から VC を生成し、proof または certificate で検査 |
| リソース | ownership、move、borrow、drop、region を静的に追跡 |
| 数値 | Int、Rat、exact decimal を基礎とし、暗黙の丸めを避ける |
| コンパイラ | Rocq を規範的 authority とし、各 pass の意味保存を証明 |
| Backend | WebAssembly を主経路とし、対象 profile を固定して検証 |
| Artifact | evidence、semantic scope、assumption、derivation を記録 |
flowchart LR
S["UTF-8 source"] --> P["Planned verified lexer / spine parser"]
P --> EL["Planned verified resolution / elaboration"]
EL --> C["NEPL Core"]
C --> K["Kernel checks"]
K --> V["VIR / VC"]
K --> R["Runtime IR"]
V --> EG["Evidence gate"]
R --> EG
EG --> W["Wasm AST"]
W --> B["Wasm bytes"]
NEPLg3 では、次の五つを直交する judgment として扱う。
- Typing
- Effect
- Resource Usage
- Termination
- Relevance
外部 solver は proof の探索に利用できるが、Certified build の authority にはしない。生成された proof または certificate を独立 checker が再検査できる場合だけ、保証の根拠として採用する。
native verification は任意の参照 backend として、Low IR -> Clight/Cminor -> CompCert の経路を計画している。主要な対話実行経路は Wasm のままである。
0.1 を最初から近似値にする必要はない。NEPLg3 は整数、rational、exact decimal を正確な表現として保持し、近似が必要になった時点で精度と丸め方を指定する。
embed Nat Int nat_to_int
embed Int Rat int_to_rat
embed Rat Number rat_to_number
FixedInt(bits, signed)
Interval(Number, precision)
これらの embed は subtyping ではなく、検査済みの明示 coercion である。Float32 と Float64 は標準数値系へ含めない。IEEE 754 が必要な platform integration だけが、任意 package の ieee754::Float32 と ieee754::Float64 を明示 import する。
一般の symbolic real equality は無理に Bool へ落とさない。証明できない比較、定義域を判定できない式、計算資源を超えた評価を、それぞれ異なる結果として返す設計である。
check が通ったことと、生成バイナリまで証明されたことは同じではない。将来の toolchain は保証を scope ごとに表示する。
Core: Kernel checked
VC: Certificate checked
Wasm AST: Semantics preserved
Binary encoding: Trusted
Host: Browser assumed
.neplcert には claim、evidence、依存関係、未解決の gap を記録し、solver なしでも再検査できる形を目指す。
| Phase | 到達点 |
|---|---|
| G0 | RFC process と phase ごとの構文、型理論、意味論、artifact、trust decision gate |
| G1a | canonical Core から WasmCert AST までの最小意味保存 slice |
| G1b | argument 境界未確定の raw item spine parser、名前解決、elaboration による Surface から Core までの経路 |
| G1c | canonical Wasm encoder と binary grammar conformance |
| G1d | compiler Wasm、one-shot ABI、Worker、memory lifecycle を含む Web 実行 |
| G2 | Dependent Core、totality、erasure |
| G3 | immutable／unrestricted value に限定した Refinement、contract、VC generation |
| G4 | Ownership、effect、LogicalView、snapshot、resource-aware VIR |
| G5 | Certificate、offline replay、trust report |
| G6 | Algebraic / transcendental を含む exact Number の拡張 |
| G7 | Wasm backend と binary encoding の保証 |
| G8 | Proof を伴う NEPLg3 self-host compiler |
最初から全機能を仮実装するのではなく、各 subset が依存する最終意味論を対応 RFC で固定したうえで、小さな実行可能 subset を縦に通していく。
NEPLg3 は、NLP / NLPS から B-debt、NEPLg1、NEPLg2 / NEPLg2.1 へ続く自作言語開発の次世代に当たる。前置記法、式指向、オフサイドルール、Web / CLI / desktop で核を共有する思想を引き継ぎ、当面は NEPLg2.1 の構文を基準に proof system と信頼モデルを設計する。
これまでの経緯は Neknaj Project — 自作言語 にまとまっている。
現在の提案書は統合仕様候補であり、正式仕様ではない。各機能の実装開始前に、そのphaseをblockするRFCだけを批准する。後続phaseのRFC全体をG1aの開始条件にはしない。
MIT License © 2026 Neknaj