SICP 会中にすごいアイデアを思いついてしまった。
いままで Guile で ACL2 のコードを書くことばかり考えてたけど、逆も可能だ。
Guile のコードから ACL2 で解釈可能な可能な限り等価なコードを生成して ACL2 で証明すればいい。こっちの方が簡単だし、まさに私のやりたいことだ。

Follow

これは無理な気がしてきた。

· · Web · 0 · 0 · 0
Sign in to participate in the conversation
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!