型の機能を増やそうってのは構わんが、
値依存型なんてのは駄目だな。
構文的な記述可能性と形式的な証明可能性がミスマッチ。
証明可能なことが事前に判っているトイプログラムならいいが、
未知な問題に対しては現実的ではないね。