Re:What I've Learned About Formal Methods in Half a Year
by sirwhinesalot on Monday April 10, 2023 @12:53PM
(#35514378)
Forall (n: Nat)
Is perfectly reasonable.
If conciseness was that important theorem provers would have syntax like APL.
Re:What I've Learned About Formal Methods in Half a Year
by tsimionescu on Monday April 10, 2023 @01:10PM
(#35514594)
Why is forall any less formal than ∀? Or Nat less formal than ℕ? Especially when these are symbols that most will have learned in high school?
Re:What I've Learned About Formal Methods in Half a Year
by sirwhinesalot on Monday April 10, 2023 @05:33PM
(#35517665)
They're not on my keyboard.
Re:What I've Learned About Formal Methods in Half a Year
by prisonguard on Monday April 10, 2023 @01:41PM
(#35514981)
there has to be a better way for a beginner to learn Lean even with the faintest high school mathematics recollection.
I can still do theorem proving in Idris excluding the mathematical notation and still learn concepts such as totality, covering, equality etc
The difficulty and verbosity of formal proofs is huge even with the very concise mathematical notation. And learning the notation itself is a very small stumbling block compared to learning the actual theorems and logic that you need to use.
So while I am not a fan of mathematical notation for general programming (which is often quite un-mathematical in fact) formal proofs are a place where this notation absolutely shines. I can't even imagine how much uglier the proof above would become if you had to replace `∀ (n : ℕ)` with something like `for any natural number n`.