Computer-Aided Reasoning: An Approach を p.49 の 3.6.3 Binary Tree まで読んで練習問題も解いた。
ここら辺の話は全体的に Lisper なら楽勝な感じだ。難しいのは ACL2 では関数を定義するときに停止性の証明に成功しないといけないという点だけど、まあ自動証明できるような書き方を教わるしあんまハマるポイントはなかった。

やりたいこと(工数: 小): S 式で表現した数式を中置式に直す手続きを書く

目的は仕事で Guile を使って計算した結果を Lisper ではない人に共有するため

やりたいこと: Mastodon on Guix System
Guix System 上で Mastodon サーバーを動かしたい。

プロジェクトに関係することは常にハッシュタグを付けて投稿しようと思う。

やりたいこと: Guile-ACL2
Guile 上で ACL2 のプログラムが動作するようにして、証明されたプログラムをそのまま Guile で使いたい。

未収載のトゥートのハッシュタグの挙動はどうなるのか気になる。
と思って試そうとしたら入力中に答えが表示された。未収載だと意味なさそう。

進捗アカウントの投稿が FTL に流れるのはちょっと申し分けないので未収載で投稿するように設定した。

Mastodon

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