Struktia
Idris で 3D CAD やろうぜ！という大分壮大な計画。
名前は Structure（構造）から
日本語名は「ストラクチア」
Idris の DSL で図形の配置を定義
コンパイルが通らなければ干渉していたり制約条件を満たしていないことになる
中間表現を吐く
そっから STL へ変換
みたいな流れ。
型レベルで安全性が担保される
内部表現には Cauchy 列を使い任意精度での数の一致、大小の比較ができる
いきなり 3 次元からやるのしんどいので 2 次元からやる
Planaktia
スライサーの計画もある
Plastika