GitHub - Kha/electrolysis: Simple verification of Rust programs via functional purification in Lean 2(!)You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
不確実さを受け入れる — A17Y (1)
ソフトウェア開発に関する認識で大きく変化したもののひとつは不確実性の扱いではなかろうか。古いソフトウェア開発が「複雑さ」を、Agile が「変化」を主要な難しさ、戦うべき敵とみなしたように、今日のソフトウェア開発は「不確実性」との戦いを大きなテーマに据えていると思う。プログラマが不確実性に向ける眼差しは開発プロセスに大小様々な影響を与えている。「達人プログラマー」とその世代は、この変化を捉えていない。 ソフトウェア開発には昔から不確実性がつきものだった。たとえば見積もりでは The Cone of Uncertainty なんて話をする。現代的なソフトウェア開発が昔と違うのは「不確実さは放っておいてもなくならない」ことを認めたことだと思う。The Cone of Uncertainty が象徴する昔のソフトウェア開発では、不確実性は一時的なもので目の前の嵐をやりすごせばいいと考える。極端に
A Formal Verification of Rust's Binary Search Implementation
This post is about my ongoing master’s thesis under Jeremy Avigad at Carnegie Mellon University, in which I’m trying to tackle formal verification of Rust programs in the interactive theorem prover Lean, and a first result of the project: a complete verification of the Rust stdlib’s binary search function. Putting the ‘Formal’ into ‘Formaldehyde’ Formal Verification is the act of mathematically re
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - leanprover/theorem_proving_in_lean: Theorem proving in Lean
Lean Web Editor
