mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
28 lines
999 B
TeX
28 lines
999 B
TeX
\section{Lessons Learned}
|
|
|
|
|
|
\subsection{Start with Arithmetic}
|
|
|
|
BFT threshold properties are the easiest to verify formally and the most common source
|
|
of bugs. Start here. The \texttt{omega} tactic makes these proofs nearly automatic.
|
|
|
|
\subsection{Model First, Prove Second}
|
|
|
|
Spend 80\% of your time getting the model right. A correct model with simple proofs
|
|
beats a wrong model with elaborate proofs. If proofs are hard, the model is usually
|
|
wrong.
|
|
|
|
\subsection{Lean~4 Is a Programming Language}
|
|
|
|
Unlike Coq or Isabelle, Lean~4 can also execute your models. Write executable
|
|
specifications that double as reference implementations. Test them against your Go code
|
|
before attempting proofs.
|
|
|
|
\subsection{Proof Debt Is Real}
|
|
|
|
When you change the model without updating proofs, you accumulate proof debt. Unlike
|
|
test debt, proof debt blocks compilation---you cannot ignore it. Plan for proof
|
|
maintenance when planning protocol changes.
|
|
|
|
%% ============================================================
|