CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech Festa 2021 winter
July Tech Festa 2021 winter で使用したスライドです。 バグのない分散システムの設計は果たして可能でしょうか？ この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。 形式手法はシステムの挙動を数学的に解析する技法で、「ノードが特定のタイミングで故障した場合にのみ発生するバグ」といった再現困難な問題を確実に検出することができます。 本講演では、CockroachDB の事例を通して、形式手法が実世界で活用されている様子をお伝えします。 イベント概要：https://techfesta.connpass.com/event/193966/ ブログ記事：https://ccvanishing.hateblo.jp/entry/2021/01/24/185819 録画：https:/
singletonsの型レベル関数を使ってしまうと示せない性質の例 - ぼくのぬまち 出張版
↓の話 実際singletonsが乱舞するんだけど，singletonsから提供されてる型レベル関数の中には使うと「それ以上証明が進まなくなる」やつが結構な割合で含まれてて，面白味のあるない以前に怒りが先行してしまう．あれは型レベル計算のためのライブラリでしかなくて証明のためのライブラリにはなれてない． https://t.co/ckCcUpWQLK— Noriyuki OHKAWA (@notogawa) January 3, 2019 サンプルコードはここ サンプルコードでやろうとしていることは「リストの反転はリスト内要素の置換の一種であることを示す」というもの まず，2つの型レベルリストが置換の関係にあることを定義する． data Permutation :: [k] -> [k] -> Type where PermutationNil :: Permutation '[] '[]
問題を解決するつもりでキッチリ型を付けた先にある高い壁 - ぼくのぬまち 出張版
null安全おじさんになりかわりそれがしがお見せつかまつる 機械が理解できる複雑な契約の型表現がもたらすものは つまるところこのようなもの ずぶぶ(切った腹から証明オブジェクトを引き摺り出す)— Noriyuki OHKAWA (@notogawa) 2016年11月18日 過ぎたるは猶及ばざるがごとし． 最近null安全？だかの話のからみで，(静的な)型で契約云々を表現してシアワセになれるんだぜーと言うのをチラホラ見聞きする．たとえば，pythonで統計なり機械学習なりやっててnumpy弄るような人が，ndarray(多次元配列)のshape(多次元配列の形)が合わずエラーで落ちたりとかそういうアレについて云々という．なるほど型があれば実行前に止めることができ，実行時，エラー*1になってファーみたいなことは避けられるだろう． しかし，これが天国へ続く道かどうかはまた別の話．(依存)型で舗
Microsoft PowerPoint - esci.pub.ppt [互換モード]
• • – • ⇒ • • • • • • – – – – – – – • – • • • – • – • ⇒ • ⇒ “Turing proved that, in general, proving program termination is ‘undecidable,’ ” Cook says. “However, this result does not preclude the existence of future program‐termination proof tools that work 99.9 percent of the time on programs written by humans. This is the sort of tool that we’re aiming to make.” • – • • – • – • • • • – • • – ⇒ •
Tests vs Types
13 January 2016 Tests vs. Types When should you use tests and when should you use types? What information and guarantees do we get for our efforts? I’ll walk through a simple, slightly contrived, example with Python, C, Haskell, and Idris. I’ll look at what you can tell about the implementation without knowing or examining it. I’m going to ignore ‘escape hatches’ which can explicitly violate the g
Theorem Prover Leanの紹介 - Just $ A sandbox
Microsoftが開発したTheorem Prover Leanを紹介します. 特徴 他の言語と軽く比較する. あくまで個人的な感想です. Lean Coq*1 Agda Isabelle 証明の書き方 structured proof, tactic, 函数定義 tactic 函数定義 structured proof, tactic 開発環境 emacs emacs, CoqIDE emacs jEdit ドキュメント × ◎ ○ △ implicit parameter ○ ○ △ (型を使わないので不要) Equational Reasoning ○(builtinなものはOK. 独自演算子は条件付き) ？(知らない) ◎ ○(基本的にbuiltinなもののみサポート) 自動証明 ×(なし？) ○(auto, omegaなど) △(emacsのautoコマンド) ◎(auto,
あるソフトウェア工学者の失敗 日本のITは何故弱いか
このドメインは お名前.com から取得されました。 お名前.com は GMOインターネットグループ(株) が運営する国内シェアNo.1のドメイン登録サービスです。 ※表示価格は、全て税込です。 ※サービス品質維持のため、一時的に対象となる料金へ一定割合の「サービス維持調整費」を加算させていただきます。 ※1 「国内シェア」は、ICANN(インターネットのドメイン名などの資源を管理する非営利団体)の公表数値をもとに集計。gTLDが集計の対象。 日本のドメイン登録業者(レジストラ)（「ICANNがレジストラとして認定した企業」一覧（InterNIC提供）内に「Japan」の記載があるもの）を対象。 レジストラ「GMO Internet Group, Inc. d/b/a Onamae.com」のシェア値を集計。 2023年5月時点の調査。
定理証明系 Haskell
この記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
ProofCafe - 名古屋を中心に活動する定理証明器・関数型言語のコミュニティ
開催勉強会 ProofCafeではいくつかの勉強会を定期開催しています。 詳細は個別のページをご覧ください。 Coqを用いたプログラムの証明について勉強する勉強会です。 コーヒーを飲みながら楽しく証明しましょう。 TAPL-nagoya Types and Programming Laungages(通称TAPL)の読書会です。 ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。 休日カフェタイム, KCTNagoya 圏論に関する勉強会です。 どえりゃあ Haskell Haskellに関する勉強会です。 サービス Software Foundations(和訳) Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧 に説明されています。 Cochin Coqの定理検索サー
Omega test and beyond
5. 最近の興味: 色々な決定手続きのオモチャ実装 • Presburger Arithmetics • Gomory’s Cut • Omega Test • Conti-Traverso • Cooper’s Algorithm • SAT / MaxSAT / Pseudo Boolean (DPLL, CDCL) • Real Arithmetics • Uninterpreted function • Fourier-Motzkin variable (Congruence Closure) elimination • 実装したいと思ってるもの • Simplex method • Gröbner basis (Buchberger) • CAD (Cylindrical Algebraic Decomposition) • (Mixed) Integer Programming
Write Yourself a Theorem Prover in 48 Hours (その4) - Qiita
去年のアドベントカレンダーの続きです！ Coqみたいな定理証明器のおもちゃみたいなのをHaskellを使って1年と48時間ぐらいで作れるかな？って話です。 去年の記事は http://qiita.com/kikx/items/10d143edc090bdfec477 http://qiita.com/kikx/items/b0eda41bc7b9036ac18d http://qiita.com/kikx/items/57aad1867b89f8955611 です。 去年の記事で型検査と計算はできたので、証明支援を行う部分を作っていきます。 対話環境の作成 対話的にコマンドを実行するコードを書くのは本質とは関係ないので、なるべく手抜きで作りましょう。ghciをそのまま使う方法もありますが、グローバルなIORefを引数で渡して回ったりしないといけないのでちょっと使いにくいです。簡単な方法とし
Write Yourself a Theorem Prover in 48 Hours (その3) - Qiita
誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。 前回 http://qiita.com/kikx/items/b0eda41bc7b9036ac18d の続きです。 今回は新しい型を追加します。 新しい型を追加する 前回までの言語には関数型と型の型しか型がなかったので、新しい型を追加します。型を追加するには以下の情報が必要です。 型のコンストラクタを表す項 値のコンストラクタを表す項 値のデストラクタを表す項 計算規則 例えば、リスト型を追加したい場合はそれぞれ以下のようになります。 型コンストラクタ list : forall A : Type, Type 値コンストラクタ nil : forall A : Type, list a cons : forall A : Type, a -> list A -> list
Write Yourself a Theorem Prover in 48 Hours (その1) - Qiita
この記事は定理証明アドベントカレンダー2013のたぶん7日目の記事です 誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。 タイトルの元ネタは http://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours です。というわけで、使う言語はHaskellですが、他の言語でも特に問題ないと思います。 定理証明器の部品は以下のものが必要です。 記述言語 カーネル 証明支援言語 その他 記述言語はCoqではGallinaといわれてる部分です。立派なプログラミング言語をひとつ設計しないといけません。このプログラミング言語によって、定理のステートメントを記述したり、証明を記述したり、関数を書いたり、データ構造を定義したりします。 カーネルは記述言語のインタープリタになります
Theorem Proverのカレンダー | Advent Calendar 2014 - Qiita
About reserved postingIf you register a secret article by the day before the same day, it will be automatically published around 7:00 on the same day. About posting periodOnly articles submitted after November 1 of the year can be registered. (Secret articles can be registered anytime articles are posted.)
誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「WindowsへのCoqのインストール」： 事情があって、AgdaかCoqを触ってみようか、と。 事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、という状況と同様です。 それでCoqのインストールは済んだのですが、処理系の使い方が分からない。個々の操作は覚えていけばいいのでしょうが、そもそもCoq処理系が何をするものなのか？ が理解できないのです。Web上にCoqの解説は幾つもあるのですが、「いやいや、そうじゃなくて、それ以前のことがサッパリわからんのですけど」という感じ。スタートラインに立てない。 それで、「Coqの解説」じゃなくて「Coqの仕様」を読んだほうがいいのかも、と https://coq.inria.fr/distrib/current/refman/ （リファレンス
Theorem proving and provers for reliable theory and implementations (TPP2014)
研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. TPP (Theorem Proving and Provers Meeting)は, 2005 年から年に 1 回開催され, 定理証明系を作っている人から使う側の人まで幅広い人たちが集まり, 様々な側面からの話をしてアイディアの交換をしてきたものです. 今年は, その第10回目になります. 多くの皆様に興味を持って頂き, 参加して頂けることを期待しています. 報告書: 研究集会「高信頼な理論と実装のための定理証明および定理証明器」(PDF 7.4MB) (溝口佳寛,Jacques Garrigue,萩原学, Reynald Affeldt編集) , MI
「美しい，だから正しい」より「正しくて，あわよくば美しい」がよい - ぼくのぬまち 出張版
関数プログラミング実践入門．発売されました．電子版もあります． 今回は本書の副題に関する話題．本書の副題には「正しい」を使っている．実際に価値を提供するのは「正しい」コードなのだが，プログラミング関連文書でよく目にするコードに対する修飾は「美しい」なのだ．これは何故だろう． といっても，大抵の人は経験などから「美しい*1」コードならば読み易く間違えにくいということを知っている．なので，この点についてそう深く考える必要は無いようにも思われる．「美しい」コードは善である． しかし，「正しさ」についてあまりにも「美しさ」に頼るようでは危険だ．「美しいから正しい」ことがわかる状態はつまり「ヒトが目を凝らすから正しい」ことがわかる状態ということに他ならない．ヒトは間違える．目も頭も疲れる． 通常，「美しい」コードに保つのは存外コストを要する作業である．お仕事であればザックリと事業戦略の正しさがまず前
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Reddit - Dive into anything
IronFleet: 分散システム検証の方法論
Write Yourself a Theorem Prover in 48 Hours (その2) - Qiita
