Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 22-Aug-2021 23:36:52 JST きゅーけー

   ACL2 の stobj を勉強してる。なんかこれで ACL2 で副作用を扱えるっぽい。構文的に更新前の過去の値が参照されないことを証明することで破壊的変更を OK とするみたい。面白い。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 22-Aug-2021 23:40:43 JST きゅーけー

     in reply to

     これだけみると更新するのに過去の値とはって感じだな。stobj は副作用のない世界で不可逆な変更をするための仕組みって感じで、副作用のある関数を導入することなく実際には破壊的な変更をするための仕組みって感じ。副作用のない世界では更新する前の変数とかにアクセスすれば、過去の値を見れるわけだけど見ないことを証明できれば破壊していても破壊していなくても差はないってことだな。