tw.log

https://twitter.com/kinaba のログ (twilog の方が便利です。)

<<newer (latest) older>>

20110801 00:20 @eldesh 「勉強会の資料に使うから参加者読めるように公開してよー」「いいよー」みたいなノリで後からweb上に上がることが結構ありますね。多分URLからしてこれもそんなんではないかと思います。追記しておきました
20110801 00:29 @lyrical_logical C++で言うと [[noreturn]] です>矛盾した関数
20110801 00:40 あなぷるに数学数学したプログラムじゃなくてもっとプログラムプログラムしたプログラム増やそうの会(終了時刻:昏倒するまで)はやりたいですよなあ。PHPとかTailsとかCertifiedとか一応そのつもりなんだけど、あまりのも簡単化しすぎて直にプログラム書く方が簡単なのでアレ。
20110801 00:49 「プログラムを手で書くより(支援下で)証明書いてextractする方が楽」な例;データ構造の不変条件保った操作なんかは脳内証明+脳内extractionで書いてるのでそれをCoqに落とせばいいんだよなーと思いつつ、所詮脳内証明は適当証明なので詳細化するとめんどいといういつもの
20110801 00:53 あるいは「callcc使って内部イテレータを外部イテレータ化する関数書け」なんてのは、何かの古典論理の命題証明しろと同値なはずで、よくわからぬままCoqに弄られてたらPeirce's lawが証明された貴方なら適当にCoq様の機嫌を伺ってればイテレータ変換も書ける!的なの
20110801 10:13 起きたらUnQL http://dx.doi.org/10.1007/s007780050084 が流行っててなんだこれは異世界に来たかと思ったら http://unqlspec.org/ 同名の別物だった
20110801 10:46 @tsukuno 自分の場合コスト関数が「0 ≒ 住む家の良さに掛かる係数<<<<(越えられない壁)<<<<< 家探し引越し等の手続き時間の短さに掛かる係数」なので、「住みたい地域近辺の不動産屋に行ってfirst-fit」 が常に最適のアルゴリズムなのでなんとも…
20110801 12:27 @tsukuno ふつう不動産屋って土日もやってるし休日でよくねーですか。
20110801 12:29 @tsukuno 大抵水曜定休らしいです(とググったらでてきた
20110801 13:40 前に @finalfusion さんから謎の呼びかけがあったのはこれかー。 http://j.mp/ojZ785 しかし僕はPike歴3時間ですしなんともかんとも…
20110801 13:48 「この言語のリファレンス/チュートリアル/ライブラリドキュメントの書き方は好きだ/嫌いだ」という感想文を140文字以内で述べる会は割と面白いかもしれない。
20110801 13:59 前も書いたけどSatherの http://j.mp/ogE7tb が割と好きで、「completeに近い説明が」「文法ベース(1.Lex… 2.Expr… 3.Decl…)じゃなく機能ベースの章立てで」「他言語との比較で独特な部分と普通な部分、を分離する指向で」書かれてるのが。

<<newer (latest) older>>

presented by k.inaba (kiki .a.t. kmonos.net) under CC0