This is from Dec 1st of last year (so not too long ago).
It's nice to see private companies dive into the (automated) theorem proving and formal verification world, and I'm curious if throwing money at this will have a meaningful impact on the field (if that is what they're planning to do). It seems like we've slowly been getting to a point, where the tools we have available now might be combined in a way that makes some impressive progress on all this.
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
Yeah 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.
You 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.
Even 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.
I 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 :)
You 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.
I’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.
None 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.
Yes 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.
That's why I was asking, I thought maybe you know more about it than those vague pointers. Lean taking in 20 million from cardano was pretty public, after all.
I have been thinking lately that perhaps in the future a lot of software will be built using DSLs, to enable cost-effective formal verification.
Turing-complete languages have an excessively broad semantics, which makes it hard to prove things about programs written with them. An alternative would be to build tools that allow engineers to develop DSLs quickly, and to then verify properties in programs written using said DSLs.
I can see some early signs of this trend in Idris, which is emphasizing DSL-building tools, or in smart contract projects, which are rushing to build contract languages with restricted semantics. There's also related work in Haskell and Racket / Scheme.
"Why do programmers go out of their way to put bugs in software?"
I wish for once people on Hacker News didn't make sweeping statements about a profession that isn't theirs? Most good designers will recognize those are bad design choices.
I think this is an endemic problem in design circles, not an exception. Also, it is not a bug but rather a deliberate intent and decision. We need more criticism, not pushback.
> "Why do programmers go out of their way to put bugs in software?"
We have no problem mocking programmers when AWS goes down, log4j or FB messes up. I expect designers from a company as big as Amazon to not fumble about the fundamentals of what makes legible text.
It is interesting that you assume I am not a designer. Regardless, design is not some mysterious profession that requires one to be a designer to criticize it.
It is actually the opposite despite of the W3 standards.
In typography, book weight for print fonts is usually lighter (congruent to W3 standards). This is because of the slight blotting effect when printed on paper. But for screen use, it is actually slightly bolder (450-ish). Here is an example from Lineto foundry: https://lineto.com/typefaces/moderne
Note for anybody who's particularly interested in automated reasoning, and likes watching video - the UCLA Automated Reasoning Group has a ton of good stuff up on Youtube.
Only if you assume x+y must be an unsigned int as well. They didn't specify the language, so you can't know that, I'd say. In a theorem prover you could prove this statement without doubt, but it's a bit weird they specified the unsigned int, to be fair.
It is great to see commercial companies starting to recognise the value of automated reasoning and other formal techniques. In my view, the difference between programming as a craft, and programming as an engineering activity, is the usage of formal methods. The same way formal models are used in other engineering disciplines when building bridges, cars, aircraft etc.
34 comments
[ 22.9 ms ] story [ 843 ms ] threadIt's nice to see private companies dive into the (automated) theorem proving and formal verification world, and I'm curious if throwing money at this will have a meaningful impact on the field (if that is what they're planning to do). It seems like we've slowly been getting to a point, where the tools we have available now might be combined in a way that makes some impressive progress on all this.
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.
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.
Two projects that did use formal methods are the beacon chain deposit contract, and (iirc) Uniswap, and both have been fine.
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.
Turing-complete languages have an excessively broad semantics, which makes it hard to prove things about programs written with them. An alternative would be to build tools that allow engineers to develop DSLs quickly, and to then verify properties in programs written using said DSLs.
I can see some early signs of this trend in Idris, which is emphasizing DSL-building tools, or in smart contract projects, which are rushing to build contract languages with restricted semantics. There's also related work in Haskell and Racket / Scheme.
I wish for once people on Hacker News didn't make sweeping statements about a profession that isn't theirs? Most good designers will recognize those are bad design choices.
> "Why do programmers go out of their way to put bugs in software?"
We have no problem mocking programmers when AWS goes down, log4j or FB messes up. I expect designers from a company as big as Amazon to not fumble about the fundamentals of what makes legible text.
I've done it before and many agree (72 upvotes): https://news.ycombinator.com/item?id=24965346
b) It looks pretty close to black to me.
In typography, book weight for print fonts is usually lighter (congruent to W3 standards). This is because of the slight blotting effect when printed on paper. But for screen use, it is actually slightly bolder (450-ish). Here is an example from Lineto foundry: https://lineto.com/typefaces/moderne
Book weight is between Regular and Medium.
https://www.youtube.com/c/UCLAAutomatedReasoningGroup
bool f(unsigned int x, unsigned int y) { return (x+y == y+x); }
undefined when x+y or y=x overflow? So no, it's NOT guaranteed to never return false. :/