Summary:
Verify also with Lean in addition to Coq.
Abstract:
Lean is the world-best in principle, however not yet a ripe, proof assistant. Add the ability to verify not only with Coq but also with Lean.
Motivation:
Lean (a kinda successor of Coq which was yet in a need of a big rewrite, creating Lean) is a nearly perfect proof assistant, in my opinion. I mean, that there is no need whatsoever to create a new proof assistant ever, we only need to modify Lean incrementally (no doubt, its libraries do require drastic rewrites or replacements, but neither Lean core nor Lean semantics needs big changes: the syntax may be improved, some minor features may be deprecated, etc., but there is no need to change the concept). It is like group theory: we may choose better symbols to denote group multiplication or omit multiplication symbols at all, but the group theory is already perfect.
So, let us choose the best and make Zilliqa verifiable with Lean.
Specification:
Write a Lean library describing Scilla and prove basic theorems about it.
For:
See above.
Against:
It is kinda fork, split of work. It needs to be carefully considered if my advice should be accepted in near future.
Poll:
- Yes.
- After about N years.
- I don’t want.