Why would an unmarked function get the broadest possible scope in a language designed for contracts? I'm always surprised by the decisions made around Ethereum, and just how much value people have poured into it.
It's a good indicator that these people may be experts in one area, but not necessarily in others.
Language design is actually notoriously difficult in general[1], but if you're doing language design for a security-critical language[2]... well, that requires actual mechanized proof, IMO. Not just proof of "design", but proof of the implementation. Anything else is a huge gamble. (And I'm sure there are some 'investors'/gamblers who made off very well.)
[1] Beyond surface-level, obviously.
[2] We're talking about 0.0001% of the general population here.
> Not just proof of "design", but proof of the implementation.
Absolutely, few people really get this. Even those that do get it generally don't know what it looks like in practice because it's so rare.
In case you're curious about what it looks like in practice (at least one way), we presented direct user code compilation and verification[1] in Jan for our smart contract language Pact[2].
The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts. For the first few days that the system started working (I built the FV portion, Stuart the language + H-M type system) I thought it was broken... turned out we just had a bug in our demo code that we never noticed.
Usually, tests check the things you know to check so when they find something it's not a surprise what they find. Sometimes you can fuzz and randomly find something, which is cool but doesn't guarantee that there isn't a problem somewhere else. However, FV just feels uncanny (as a dev) because the test either finds a problem in the code -- and tells you how to replicate the bug -- OR proves that a problem cannot exist.
> The idea that you can write a doc test that triggers a formal verification about some aspect of your code is, for lack of a better term, strange and yet the power to weight ratio is just off the charts.
I'm not sure I understand this sentence. Are you doing doctests, or are your doctests statements of formal properties, or have you abandoned that and are now doing formal specs->code type things?
It's closest to the middle, assuming that you meant that you're stating the properties that you want to test. It does more than that, but at its base that's effectively how it works so it's close enough for a solid intuition. We're working on a paper about it now -- or at least a sub-paper in the clutch of papers that pertain to a public chain version -- that I'll link to when it's out (a couple weeks probably).
Why bad timing? This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. "One of the best Solidity devs" just failed to write a safe contract to the tune of a $30M exploit. Given that, what chance does anyone else have?
At some point, it's time to blame the tool and not the user. Moreover, it's not like people didn't see this coming, myself included[1]. I mean, who really thought that basically taking JavaScript and swapping out the DOM for a bank account wasn't going to end badly? But then again, maybe I've spent too much time at in the SEC/finance where "move fast and break things" engineering gets you shown the door quite quickly. That mantra's fine for a number of domains but finance isn't one of them as one bug can bankrupt the company (see: knight capital).
It really just underlines the need for a safer/better approach. Formal Verification has to be part of that story. A language that was designed with safety in mind has to be another part.
Also, not an academic (yet at least). Cofounder here: http://kadena.io
Read the Solidity documentation on visibility [1]. Public, private, internal, external, that really seem to mix overlapping concerns. In the visibility documentation, it explains that the default is public.
Then, in another section of the documentation, when talking about function types [2], not specifying internal or external defaults visibility to internal.
It doesn't seem like the simplest or most consistent way to express these concepts, and certainly not the safest way.
Your honour, in my defence, the contract clearly specified that anyone could reset the wallet, and if that's not what they wanted, they shouldn't have agreed to it.
That's not how JavaScript works. Variable declarations are hoisted to the start of the enclosing function scope and only undeclared variables are global by default.
But yes it seems pretty asinine to use global by default for (not so) smart contracts.
Another way of describing that is that variables are global (scoped to the lobby, to borrow a term from the languages which came before JavaScript) unless explicitly marked with the "var" keyword, which has semantics that some languages might have chosen to give the name "local". Like: your entire premise that a variable is only the declared variables makes no sense to me as someone who teaches college-level classes in programming languages. In Python variables default to local unless marked "global". In JavaScript, variables default to captured via scope unless marked "var".
Well, if they are global when they are undeclared, that pretty much means they are global by default. Maybe a better way of putting it would be "js variables are declared global by default, when unspecified and not using strict mode".
Anyway, I think parent's point was to say this behavior already has been seen in javascript. Actually, it may even be inherited from javascript. When I first looked at solidity last year, I was under the impression it was a modified version of javascript, like unity3d's one. Nowadays, solidity landing page reads "high-level language whose syntax is similar to that of JavaScript", so not sure if it still is (or has ever been, for the matter) derived from something like v8 or rhino.
The reason for that choice seems not far fetched : it's not uncommon, when wanting to add scripting to something, to go with javascript, since it's arguably the most known language, developers knowing "<their main language> and javascript", especially webdevs (a blockchain app project, lisk, even made html/css/js the defacto mean to build apps). Of course, fintech is an industry where the usual values from webdev (release early, release often) have disastrous results.
In javaScript, the following lines does different things:
"use strict";
foo = 1;
var bar = 1;
"foo=1" changes the variable foo (this is very useful) and "var bar=1" creates variable bar and adds it to the function/lexical scope. If the variable foo is not created/declared, it will throw an error! But without "use strict", "foo=1" would add variable foo to the global scope! Which might create unexpected bugs if you are used to other languages that does the sane thing and adds it to the local function/lexical scope. So I suggest to always "use strict" !
Language design is actually notoriously difficult in general[1], but if you're doing language design for a security-critical language[2]... well, that requires actual mechanized proof, IMO. Not just proof of "design", but proof of the implementation. Anything else is a huge gamble. (And I'm sure there are some 'investors'/gamblers who made off very well.)
[1] Beyond surface-level, obviously.
[2] We're talking about 0.0001% of the general population here.