They are a band of dudes who want to repaint the world in OCaml. It makes sense they try to make people working on the Coq proof assistant (there is a very strong relation with the ML and the OCaml world), now that they have some money: it is not easy to find this kind of guys. For instance, with Coq after several years (more or less 10 years I think) Leroy and his team have been able to build/prove a "small" C compiler down to the generated assembly code (http://gallium.inria.fr/~xleroy/bibrefs/Leroy-compcert-06.html), this is a really huge effort to make each algorithm and all the proofs around it .
In my humble opinion, I think the project is too complex, too ambitious, even if it will bring interesting stuff. I prefer the pragmatism around EOS built around production proven code, and its "simplicity": it is even more important that any developer using EOS fully understands the mechanic under the hood.
You are viewing a single comment's thread from:
Correctness is a crucial feature for smart contracts. When there are high stakes, you want to be certain that your application is proved to follow its specification.
I do agree fully on correctness.
But, I think it is a race against the clock with 12/18 months time frame to catch on, even if ICOs are reaching crazy numbers if one or two of your main competitors already took a major part of the market, it will be very tough if you do not have a few magic features.
When thousands of dollars, if not million, worth of tokens/contracts are compromised, people have a better product to go. I agree with the time frame, but for this market being wrong will be costly.