4 ms·
I think realistically the biggest source of research money is from blockchain projects as so many use formal methods nowadays, and have done for a couple years
by exdsq 5y ago
I think realistically the biggest source of research money is from blockchain projects as so many use formal methods nowadays, and have done for a couple years
- sva_ 5y agoIt doesn't seem their formal methods are all that good for verification, looking at all the smart contract exploiting going on? edit: It's ridiculous how you get downvoted for just asking a question in an unrelated thread. Just shows how rotten this whole space is.
- exdsq 5y agoYeah for sure, but the underlying chains are pretty solid, and some of the languages are particularly well formalized such as Plutus (which is led by SPJ’s son with a few of the original Haskell language team). But you can’t save people from bugs higher up the stack when it comes to turing complete contracts. It can definitely be better though.
- mbrodersen 5y agoYou are getting downvoted because your reasoning is flawed. Smart contract exploiting has nothing to do with whether formal reasoning works or not. It’s as incorrect as saying that cars doesn’t work because your car doesn’t work.
- DennisP 5y agoEven if formal methods could make your contracts bulletproof, they don't help at all when people don't use them. The barrier to entry in smart contract development is pretty low, and lots of people don't do everything they should to minimize risk. Two projects that did use formal methods are the beacon chain deposit contract, and (iirc) Uniswap, and both have been fine.
- exdsq 5y agoI know - I no longer care about Karma on HN because if you chat about crypto regularly it’s entirely based on which Pro vs Anti group has seen it more. +1 from me because the space needs good questions :)
- the_benno 5y agoYou can argue that it's growing and/or promising, but there is absolutely no way that the actual research funding coming out of blockchain-land can hold a candle to the big formal methods labs at major tech firms or traditional academic research funding.
- exdsq 5y agoI’m not sure to be honest because I don’t know how much comes from major tech firms - but I do know someone who financed their own research center and have seen probably billions in the last year or two so it feels like a sizeable amount compared to standard academic funding for fairly niche stuff. And if you look at it from a technical perspective where your options are TLA+, Coq, Agda, Isabelle, etc, I think you’ll find most of the core devs are involved in blockchain somehow nowadays. At least that’s what it feels like.
- deleted 5y ago[deleted]
- auggierose 5y agoWho of the Isabelle core devs is involved in blockchain?
- the_benno 5y agoNone of them -- Isabelle is developed at University of Cambridge and TU Munich by academics. The parent commenter seems to have some mistaken notions and assumptions about formal methods and PL research.
- exdsq 5y agoYes but a lot of academics moonlight in blockchain as consultants on their tools. Some are more public than others, such as PL guys like Philip Wadler, but just because they’re a professor at a university doesn’t mean they’re not also working on external startups.