Please do not try to understand Lean or proof assistants without first getting a rudimentary understanding of the logic involved. This article sort of skips over it, which is reasonable because it is pretty involved.
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
* Proof trees - <a href="https://en.wikipedia.org/wiki/Method_of_analytic_tableaux" rel="nofollow">https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
What you actually need is knowledge of an overview of the Mathematics of Formal Methods in all their aspects viz. Predicate Logic, Set Theory, Temporal Logic, Type Systems etc.
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.
fooker · · focus · HN ↗
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
* Proof trees - <a href="https://en.wikipedia.org/wiki/Method_of_analytic_tableaux" rel="nofollow">https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
* Constructive/Intuitionistic logic - <a href="https://en.wikipedia.org/wiki/Intuitionistic_logic" rel="nofollow">https://en.wikipedia.org/wiki/Intuitionistic_logic
* Proofs and Types - <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
* (In)completeness - <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems" rel="nofollow">https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
* Compactness - <a href="https://en.wikipedia.org/wiki/Compactness_theorem" rel="nofollow">https://en.wikipedia.org/wiki/Compactness_theorem
rramadass · · focus · HN ↗
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
whattheheckheck · · focus · HN ↗
I thought this AI or SI was supposed to make shit easier for everyone.
rramadass · · focus · HN ↗
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.