Earlier quoted context omitted.
>I'm curious: could any of the recently known smart contract bugs have been prevented through the use of a stricter type system? Short-answer is yes, and there's been lots of work done to go even further than having static typing and have formal verification for smart-contracts. >I'm genuinely curious: what types of bugs does a stricter type system catch that a reasonable test suite probably would not? Not sure what…
> Short-answer is yes, and there's been lots of work done to go even further than having static typing and have formal verification for smart-contracts. Yes, I've looked at some of these projects before. And I certainly think it's a good idea to use automated tools to try to prove properties about programs. But I'm more excited about things like property testing than I am about things like strong type systems. And I'…
> But I'm more excited about things like property testing than I am about things like strong type systems. And I'm wondering specifically what is the value they bring.
By "property checking" you mean theorem proving.
Static type checkers are theorem provers. More powerful type systems allow more interesting and less intuitive proofs to be written. Sometimes, the type checker is integral to the compiler and is required to run on every build, and sometimes it's an external tool.
In any case, if you're adding annotations to your source code in order for a theorem prover to statically prove certain runtime properties, those annotations constitute a static type system which is type-checked by your theorem prover.
Maybe you don't like even a subset of your theorem prover to run on every build, but if you're in favor of machine-checked proofs of program behavior, you're in favor of static typing.