制度を仕様記述に落とし込んで形式検証にかけることによって集合論的な抜け漏れの検査に使えそうなことは分かったけど、述語論理と条文の一致を検査するために人手を要するのでは、全体として工数が減るのか分からない。
台帳が持つ本人についての記録と、条文上の該当性とのマッピングも、やろうと思えばSMTソルバーを使えるけれども、それが効率的か、そこまでやる必要があるのか、関数に落とし込んだ方が軽いのではないかという論点もある。予め事務まで考えた制度であれば、割と簡単に関数なりSQLに落とし込んで該当性を判定できる。
複数のデータコントローラーから集めたデータを串刺しで集計して、制度の該当性を判断する仕組みは、今のワンストップサービスやらブッシュ型サービスの仕組みでは難しいところ、ウォレットの先にそういった世界観をつくることは技術的にはできそうではある。
ではそこで集積した属性情報に対して、制度の該当性を解釈していくロジックを組み立てる上で、それぞれの制度を述語論理で記述してSMTソルバーにかけるのがいいのか、もっと簡単なロジックを端末側に持たせるだけで済むのかは、実際にプロトタイピングを通じて検証した方が良さげではあるな。