『定理証明支援系 Coq チュートリアル』に参加した
先週の土日にこのオンラインセミナーに参加してみた。
定理証明は、名前は聞くけど触ったことはなくて、興味はあるけど本を買うほどのモチベーションはないし、誰か詳しい人が要点だけ教えてくれたりしないかな〜。と思っていたところ、まさにぴったりのイベントが。なんていうか、昔ならこういうのは東京まで行かないと参加できなかった気がするけど、家からオンラインで参加できるようになったのは嬉しいね。
日程は5時間 x 2日という長丁場で、説明だけでなく練習問題もあるのでとっても疲れた!でもこういうのって自分で手を動かさないと「わかったような気になった」だけで終わりがちだから、演習があるのはとてもありがたい。
Coqの感想
2021年6月 (Shiika enum)
近況です。
Shiika
今月はenumを実装した。ようやく念願のOption型が使えるようになるぞ…と思いきや、パターンマッチがないのでメソッドが書けないことが判明。道は長い。
ちなみにクラス名はOptionじゃなくてMaybeにする予定。HaskellとRakuくらいでしか見たことないけど、コンピュータぽくなくて好きなんですよね。あとOptionという名前はCLIアプリで普通に使いそうとか、Maybeの方が(日本人にとっては?)初学者に意味がわかりやすいとか。
BiwaScheme
2021年5月 (処理系ミートアップ)
近況です。
Shiika
今月は定数まわりの実装を整理した。これでenumが実装できる…と思ったんだけど、その前に「スーパークラスに型パラメータを書けるようにする」が必要であることが判明した。yak shavingだなあ。しかしまあ先に気づけてよかった。ミートアップのおかげだ。
BiwaScheme
2021年4月 (Shiika 分割コンパイル)
2021年3月 (simple_twitter)
近況です。
Shiika
今月はいろいろ他事をしていてあまり進められなかった。if文の型チェックを整理したくらいか。これでこういうのが書けるようになった。
次は分割コンパイルの件に手を付けたい。
BiwaScheme
2021年2月 (Shiika return)
先月の活動報告です。
Shiika
doc/guide, doc/specを追加した。一見同じものに見えるが、前者はユーザ向け、後者は仕様書なので微妙に内容が違う。例えば「メソッド名は慣習的にunder_scoredにする」という話は前者には書くが、後者には書かない。一方、普段使わないようなコーナーケースの話は後者にだけ書く。という感じ。
あとメソッドからのreturnを実装した。その勢いでブロックからのreturnも実装しようとしたのだが、思ったよりはるかに難しいことがわかり一旦ペンディングにすることにした。
BiwaScheme
2021年1月 (TENET)
近況です。
Shiika
今月はなんかいろいろやった。大きなのはHashクラスが入ったのと、Array#mapが入ったのと、こないだ書いたctxのリファクタリングかな。
あとは「一年の計は元旦にあり」ということで、Shiikaレベルで書けないものをどうするか検討していた。結果としては、標準ライブラリはRustで書いて、それとは別にffi機能を提供するということに落ち着きそう。Rustでライブラリ(RubyでいうRubyGemsみたいな)を書けるようにしようかなとも思ったのだけど、それだけだと例えばlibSDLを使いたいときにShiika→Rust→Cという二人羽織状態になってしまうので。
BiwaScheme
2020年
2020年の振り返り。
イベント
今年はほとんどのイベントがオンライン化するという未曾有の事態だった。登壇としては10月のlangsmith1件で、これもオンライン。
開発
Shiikaの開発が進み、だいぶ「本物」に近づいてきた。advent of codeとかで実際にShiikaプログラムを書いてみてるけど、体験はとてもよい。まだまだ荒削りだけど、方向性が間違っていないことが確認できたといえよう。
2020年12月 (AdventOfCode)
近況です。
アドカレ
今年は2本。
- Shiika進捗2020 - yhara.jp
- 今年やった主な作業をまとめた。
- 28キーのミニマルなキーボード、Alpha - yhara.jp
- Alphaが完成したので書いた。28キーでも工夫すれば仕事で使えるレベルになる(含プログラミング)ことがわかった。