#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
-
yoshihiro503
- 5175
- 0
- 4
- 14
-
- いいね！14
Sosuke MORIGUCHI
@chiguri
今井さんの発表。 Coqを使ったデジタルデータ放送におけるストリームデータ処理の形式化と検証 #TPP2014
2014-12-04 09:33:05
Sosuke MORIGUCHI
@chiguri
民間企業なのでお金を稼ぐことを目的としないといけない（「稼げなくなったら、死ということですね」） #TPP2014
2014-12-04 09:34:12
Masahiro Sakai
@masahiro_sakai
#TPP2014 二日目、 yoshihiro503さんの招待講演「Coqを使ったデジタルデータ放送におけるストリームデータ処理の形式化と検証」(今井 宣洋) 民間企業でCoqをどうお金儲けに使っているかという話とのこと。
2014-12-04 09:34:26
Masahiro Sakai
@masahiro_sakai
独立系なので常に仕事をとってこないと死だが、基本エンジニアだけの会社。 納入したソフトウェアの品質→信頼→営業になる。 品質のために静的型付き関数型言語やCoq。 #TPP2014
2014-12-04 10:01:50
Takashi Miyamoto
@tmiya_
仕様やアルゴリズムを検証した、ということと、検証済みの実行可能コードを生成出来る、ということの区別がついてない？ #tpp2014
2014-12-04 10:15:21
Takashi Miyamoto
@tmiya_
仕様を満たすこと検証可能な最低限のテストケース、という話はむかし @kinaba さんがなんか述べてた気がする。。 #tpp2014
2014-12-04 10:18:59
Takashi Miyamoto
@tmiya_
まぁ慣れてれば、（証明を除けば）関数の実装速度はCoqでもOCamlでも大差ないと言えば無いよなぁ。#tpp2014
2014-12-04 10:25:24
Sosuke MORIGUCHI
@chiguri
@tmiya_ まあものに依りますね。今回のはCoInductiveなので停止性気にしないで良いですけど。 #TPP2014
2014-12-04 10:26:21
Masahiro Sakai
@masahiro_sakai
@Alcor @yoshihiro503 たしかWhyのグループとかは、verificationのために形式的仕様が必要だが、現場のエンジニアが書いてくれないという問題に対し、形式的仕様からのテストケース生成を現場にも分かりやすいご利益／入口にしようとしてたはず #TPP2014
2014-12-04 10:34:18
Masahiro Sakai
@masahiro_sakai
招待講演「システム開発において数理論理学に基づいた仕様記述言語を用いることによる品質の確保 ～文書の記述力とチームのコミュニケーション力を鍛える～」（栗田太郎／フェリカネットワークス） VDMの話かな。 #TPP2014
2014-12-04 10:43:21
Sosuke MORIGUCHI
@chiguri
大人数だとコミュニケーションの問題などがあるので、大人数チームでもできる限り正確にしたい。まず曖昧な日本語仕様書は論外。 #TPP2014
2014-12-04 10:51:43