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

OCamlコードをCoqで検証できる "CFML" で証明コンペに挑戦 (未完) - keigoiの日記
VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るのは見送った（というかチームの人数上限4人で入れなかった）。仕事や出張の片手間でやっていたので、結局一問も検証できなかったけど、楽しかった。検証にはCFMLというツールを勉強しながら使った。これを使えば OCaml のソースコードを Coq で検証できる。それも ref型による破壊的代入つきの手続き的なOCamlを含む。そして Coqと違い、プログラムは停止しなくてもいい。つまり、CFMLを使えば、手続き型プログラムを、ホーア論理+分離論理(のようなもの;後述)を使って
sh19910711 2024/03/22
"ソフトウェア検証のコンペ / CFML: OCaml のソースコードを Coq で検証 + 手続き的なプログラムも検証できる。 Dijkstra の最短路アルゴリズムなど / 使いこなせれば幸せな世界が待っている" 2011

*program

contest

coq
リンク
Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記
Haskell Advent Calendar jp 2010のためのエントリです（17日目）． 6日目の id:camlspotterさんの経験15年のOCaml ユーザーが Haskell を仕事で半年使ってみたに対するカウンター（になってるかどうか分からないですが）みたいな感じです．近くて遠い隣人：HaskellとOCaml OCamlはHaskellと違って副作用があり，更にHM型推論をもつためプログラマは本質的な部分の記述に注力しつつ，コードのチューニングもできる．つまり働くHaskellプログラマがシリアスなソフトウェアを書く時に使えるほとんど唯一の選択肢だ．しかし，同じ静的型付けの関数型言語でありながら，OCamlとHaskellの見た目はかなり異なる．この記事では， HaskellプログラマがOCamlを使い始めると，どういうトラップにハマるかを書く．なかでも，
sh19910711 2013/04/16
*program

func*
リンク
実務で使うOCaml - 泥臭い仕事をサクっとこなす方法 - keigoiの日記
プログラマが実務で出会うのは、問題が整理されたキレイな仕事ばかりじゃない。プロダクトに本質的じゃない部分でもプログラムを書く必要に迫られる。いわゆる開発方法論では抽象化されてしまう、今ここにいるソフトウェア開発者の悩みだ。今日は、私が仕事で書いたOCamlのコードを晒して、如何にOCamlがプログラマの仕事の道具として優れているかを主張したい。泥臭く、関数的でない、エレガントさのかけらもない、生活臭のあるコードだ。勤務先はOCamlをメイン言語として使っている。研究所とかではなく普通に受託開発を生業としている会社だ。OCamlは理論一辺倒で、マニア向けで、現実のソフトウェア開発には使えない、という誤解が万が一あるかもしれないが、全くそんなことはない。 (Haskellもそうだけど、それはまたの機会に) いかにOCamlが優れているかについての概論めいた話は、OCamlを数十人体制で10年
sh19910711 2012/11/25
*program

func*
リンク
1