smoking186のブックマーク - はてなブックマーク

停止性問題は決定不能→バグのないソフトウェアは作れない？ - sumiiのブログ
「チューリングマシンの停止性問題が決定不能だから、バグのないソフトウェアは作れない」という説を（アカデミックな人からも）よく聞く*1のですが、（結論はともかく）論理が理解できません。「停止性問題が決定不能 → Completeな自動検証器は実装不能 → バグのないソフトウェアは作れない」の２番目の矢印が成り立たないと思うのですが、別の意味？（もちろん、今のCoqやCharityですべての業務プログラムを記述しろ:-)とか言うつもりはありませんが） P.S. bonotakeさんからコメントをいただきましたが他の方のために：「Completeな」（バグがあれば必ずyesと答え、バグがなければ必ずnoと答える）という限定条件もついているので注意が必要です。バグの種類にもよりますが、単にsound（バグがあればyesと答える＝noと答えたらバグはない）とか、「十分に近似」とかであれば、実装可能な
smoking186 2009/03/11
リンク
Xさん - sumiiのブログ
某Xさん（国外研究者）は、Sumii & P氏の論文と序論が一字一句までほぼ同一の論文を投稿したり*1（序論以外の内容はまったく違ったのでまあ良い？のですが）、何の根拠もなく「Sumii & P氏の手法より単純」と主張する論文を発表したり、その論文のmain theoremが間違っていた（定理が成り立たず、修正方法も明らかでない）にも関わらず訂正しないでホームページにおいてあったりして、極めてイメージが悪かったのですが、話してみたら感じの良い人で、おもしろそうな研究テーマまで提案してくれました。むう？ *1:Xさん曰く「メモに書き留めておいたフレーズを使ってしまった」とのこと。お前はな○ちか！
smoking186 2007/10/12
scientist
リンク
POPL 2007実況その2 - sumiiのブログ
朝食 ilogのAit Kaci氏（初対面，Jacques Garrigue氏の元ボス）やMS Researchの人たちと話．セッション1 またFelleisenが自分でsession chair．招待講演を3件とも「非POPLな人」にしたことについて語っている．「モジュールやマクロの話は飽きた」？ Don Batory氏．ソフトウェア「工学」の人．代数や理論の知識が「普段の業務で」役に立つという話らしい．domain specificな高級言語のほうが最適化しやすい（古典的な例: SQLと関係代数）とか．継承は差分プログラミングに便利ではあるが，十分ではないのでmixinの一種が必要で，そのmixinの一種による差分プログラミングは代数的に形式化できる，とか．MakefileやXML文書にも同様の構造がある(?)とか．差分プログラミングによるソフトウェアの合成をカテゴリー理論(??)で
smoking186 2007/01/27
_Computer

conference&workshop

programming
リンク
学者も宣伝するのです - sumiiのブログ
勉強じゃなくて宣伝のほうは、と考えたのですが、たとえばUNIX MagazineやSoftware Designみたいな「一般むけ」の雑誌に、「OCamlへのイントロダクション」とか「『普通のプログラマ』のための情報系学会紹介」みたいな原稿をいきなり送りつけたら（文章や中身はまともだとして）載せてもらえるのでしょうか？　それとも、やはり紹介が必要でしょうか。あるいは、どうやっても掲載は無理…？
smoking186 2006/04/07
_science
リンク
1