Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 141

まあ、たしかに現実のソフトウェアと比べれば簡単すぎる例だけど、ハフマン符号化したやつを正しく復号できるとかまで証明できるようになってきたらなんというか面白くなってくるのは分かるっしょ。

定理の命名が雑過ぎてよくないなこれ……。

私が過去に書いたやつでいちばん感動したのは SICP のハフマン符号木まわりの練習問題を ACL2 でやって、ある程度の性質を証明できたときだったと思う。ACL2 用に用意された問題ではない問題でも証明できる体験をすることでモチベーションが上がってきてる。

https://git.tojo.tokyo/sicp-acl2.git/tree/huffman-tree.lisp

そもそも ACL2 産業界で既に結構使われているし机上の空論ではない。

https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/?topic=ACL2____INTERESTING-APPLICATIONS

関数が第一級であるということを捨てさえすれば、自動定理証明がそこそこうまくいくのは使ってる感じ結構実感できてる。

書くプログラムを一階述語論理の範囲に限定すれば完全性と健全性が保証されるので希望がある。ACL2 はそういう戦略をとってる。そのために課せられた制約はキツいけど使ってる感じなんとかなるという感じはする.。

たとえば i32 / i32 はクソなので i32 / NonZeroI32 だけを用意しろみたいなの、まあまあ正論ではあるんだけど、そのためには定理証明が必要になって、そして定理証明って案外非力なのよね。少なくともコンパイラに組み込んであらゆる場合に強制してやろうと思えるほど都合の良いものではない

私は静的型付き言語の Optional 型とか Maybe 型が基本的に嫌いなんだ。それが使われるのは外界とのやりとりに限定されて欲しい。私はそれが失敗しないと分かっているのに証明できている訳でないから Maybe にしたくなるのはクソ過ぎる。そういうのは定理証明すればいい。

私は静的型付き言語も好きなんだけど、私は絶対に失敗しないと分かっているのに Maybe 型とかを使いたくなってしまうような状況がもの凄く嫌で、そういう状況が限りなく少なくなるようなプログラミング言語を求めてしまう。Typed Racket は正の整数型とかがあるので、普通の静的型付けのプログラミング言語よりはちょっと強いけど全然足りない。

そういう理由があって私は ACL2 のような定理証明支援系に手を出しているわけだ。

Typed Racket が使えるかどうかは Occurrence Typing に適合できるかどうかにかかってる。

5 Occurrence Typinghttps://docs.racket-lang.org/ts-guide/occurrence-typing.html

Typed Racket は型推論がちょっと弱めで、割と型を書かされるのはつらいかもしれないけどそれさえ耐えれば普通に良いと思う。

Typed Racket のやつは本格的なんで TypeScript のやつとかとは全然違うのであまり gradual typing とひとくくりにしない方が良い感はあると思ってる。TypeScript の any みたいな全てを破壊するようなやつは Typed Racket には存在しない。

まあ、今の私は ACL2 に夢中なんで ACL2 ならそれくらいのことができるのは当然なためもはやあんま嬉しくないが。

Typed Racket は数値型が豊富で Natural 型があったりするの好き。負の数を静的に拒絶できる factorial 手続きとかが書けるので強いぞ。

あとは ACL2 みたいのを導入するとかかな。ACL2 で証明したやつを Guile に持っていきたい野望は持ってたんだけどもうほぼ挫折してる。Scheme と Common Lisp のサブセットじゃ意味論違うし。

というかよく考えたら Typed Racket が存在するじゃん。あれも普通の Racket の世界とやりとりできるし、Typed Racket は普通にちゃんとした静的型を持った言語なのでいい。

Guile じゃなくて Racket を導入すれば解決っぽい雰囲気あるな。まあ、Typed Racket はマクロでしっかりとした静的型を実現できることを示した例なんで、Guile でも同じことをやれば技術的に可能なことは間違いない。

これだ、こうやって部分的に静的型を導入できるんだからできない理由は確かにない。

Introducing Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp | The Coalton Languagehttps://coalton-lang.github.io/20211010-introducing-coalton/

そういえば最近 Common Lisp に静的型付け言語を埋め込むやつが話題になってたな。たしかに静的型付きでも可能ではありそう。

でもまああれは半ばバイナリなのでちょっと扱いが難しいといえば難しいんだけど……

静的型付きが好みな世界で生きてるマンとしては、そういう機能拡張まわりは WASM / WASI に期待しているし、そのうち何か実装してみたさもある