3 ms·
I would go further. Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties o
by johnbender 10y ago
I would go further.
Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties of these blockchain programs (beyond type safety).
Not every application would require that kind of rigour but if the participation and value of a given currency/contract/program is determined largely by trust then it seems natural to want more serious guarantees.
- willtim 10y agoI agree. I covered this only briefly under 'formal methods'. My point was that such formal semantics and proofs are far more easily obtained starting from a functional language.
- mietek 10y agoNote that a type system, if done properly, is simply another name for a logic for proving properties of programs. Examples: * Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) * Coq (https://coq.inria.fr https://coq.inria.fr) * Idris (http://www.idris-lang.org http://www.idris-lang.org)