https://twitter.com/kinaba のログ (twilog の方が便利です。)
| Coqとかを『「正しい」プログラムを書くための言語』としてみると見誤ると思っている。 | |
| 単純に、プログラムとか関係なく、証明を書くための言語、と思いたい。CurryHowardとか持ち出すまでもなく、「モジュール化が重必要」「抽象化も重要」「究極的には組み込みの細かいステップの組み合わせで書かなければならい」ものの設計にはプログラミングと同じ考え方が使えるというだけ | |
| s/重必要/重要/ | |
| 「プログラム」と「証明」の場合には、たまたま、それを同じ単一の言語でやることに意味がある、のだと思う。『「証明済みである」という型』をプログラムで使えると嬉しいし、逆に、四色問題のようなプログラムドリブン証明をするときにそのプログラムが証明になってることを確かめたいとか。 | |
| 少なくとも、なんか、初歩の初歩からプログラムと証明が出会うところまでには明らかに距離があるので、「そこは離れているモノ」と思って入門しないとだいぶアテがはずれると思うのだよね | |
| 【急募】 brainfuckのソースレベルデバッガ | |
| @naoya_t おーかっこいい！ちょっと今最低でも30KBはあるBFのソースをデバッグしたいのですがどうしたものかと頭を抱えているところでして… | |
| wWWwwww でやっと 'w' が出た！ | |
| wWWwwww のコンパイル結果→ http://www.kmonos.net/wlog/sub/w.txt | |
| HelloWorldくらいは動いてると思うんだけど遅すぎて最初の'H'すら全然出てこない | |
| @naoya_t www | |
| 例によって誰も読みそうにない日記かいた | |
| brainf*ckでプログラムを書くのは（チューリングマシンでプログラムを書くより遙かに）難しい | |
| 今みたいにスキマの量を状況に応じて変えるんじゃなくて、データは3n+0番目にしか入れない、3n+1番は作業領域、3n+2番はグローバル変数持ち回り用領域、と決めた方がかなり綺麗になるような気がしてきた。って何をマジメに考えているんだ俺は | |
| @naoya_t 1getとかするほど伸びないと思うwWWwwwwWWWwWWWWw | |
| さて帰ろう |