News for hackers. Stuff that matters.

A comment on Formalizing Text Editors in Coq. Parent comment

Re:Formalizing Text Editors in Coq by orbifold on Tuesday June 09, 2020 @04:49AM (#23464935)
Checkout Lean, the lead developer also started Z3 . Lean 3 is implemented in C++ and apparently is much faster than Coq. They are in the process of implementing Lean 4, which will feature native code generation and might become one of the first practical dependently typed programming languages.
[ Parent | on HN ]
Re:Formalizing Text Editors in Coq by tom_mellior on Tuesday June 09, 2020 @07:48AM (#23465752)
> Lean 3 is implemented in C++ and apparently is much faster than Coq.

1. The parent didn't comment in any way on Coq's performance, they barely mentioned Coq at all.

2. Coq is implemented in OCaml, which produces pretty good code. If Lean is faster than Coq, that's more likely due to more optimized algorithms or data structures.

3. Your wording using "apparently" suggests that you don't even have practical experience with this, you just want to promote a software system you have never used?

What is the point of a comment like this?

[ Parent | on HN ]
Re:Formalizing Text Editors in Coq by h91wka on Tuesday June 09, 2020 @06:44AM (#23465417)
Lean 3 is community maintained, aka dead. Lean 4 is described as "go away", and it will be incompatible with Lean 3. So much for practicality.
[ Parent | on HN ]