Yeah, I bike regularly on and off (season/mood/goals dependent, honestly), and knowing what I should expect on my commute to work /and/ back is important... and not something I can predict without looking at the weather in the morning.
I guess I'd say -- I think you're right that you shouldn't (ideally) be able to trigger true deadlocks/livelocks with just serializable transactions + an OLTP DBMS.
That doesn't mean it won't happen, of course. The people who write databases are just programmers, too. And you can certainly imagine a situation where you get two (or more) "ad-hoc" transactions that can't necessarily progress when serializable but can with read committed (ad-hoc in the sense of the paper here: https://cacm.acm.org/research-highlights/technical-perspecti...).
I mean, you say that, but systems like Spanner exist & I think the fact that it's used for Gmail, Docs, etc. has demonstrated that for a large range of OLTP workloads, serializable everywhere and also performant /is/ possible to architect for -- with the right combination of both database + application design.
That isn't to say it's correct everywhere, but I'd maybe be a little more suspicious of "We want OLTP but we can't use serializable" in a vacuum.
Of course--there are obvious cases like "We can't use serializable because of how our database implements it" or even "because we can't be arsed to figure out how to structure all our data accesses to avoid conflicts and aren't paid enough to solve that problem", but I feel like those are a bit more honest than "Because of performance reasons, in all cases". :)
You can, with some programming languages, require a proof of this (see: Rocq, formerly 'coq').
I think a more interesting case might be showing functional equivalence on some subset of all inputs (because tbh, showing functional equivalence on all inputs often requires "doing certain things the slow way").
An even more interesting case might be "inputs of up to a particular complexity in execution" (which is... very hard to calculate, but likely would mean combining ~code coverage & ~path coverage).
Of course, doing all of that w/o creating security issues (esp. with native code) is an even further out pipe dream.
I'd settle for something much simpler, like "we can automatically vectorize certain loop patterns for particular hardware if we know the hardware we're targeting" from a compiler. That's already hard enough to be basically a pipe dream.
I mean, in C++ (17? 20? Whenever constexpr was introduced) it's totally possible to create a library that allows you to build a SQL query via the language's string concatenation libraries/etc., but only allows you to do it with static strings unless you use ~shenanigans. (C++ unfortunately always allows ~shenanigans...)
I guess you do wind up needing to potentially re-implement some basic things (or I guess more complex, if you want format string support too). But for basic string concatenation & interpolation, it's reasonable.
That's a pretty useful way to get basic string concatenation while also preventing it from creating opportunities for SQL injection.
For example, you have a class that requires a constexpr input & can be appended to/concatenated/etc.:
SqlStringPart(constexpr ...)
operator+(SqlStringPart ...)
(so on)
And you have a Query API that only takes SQL string expressions that are built out of compile time constants + parameters:
SqlQuery(SqlStringPart ..., Parameters ...);
This doesn't solve the problem mentioned in the article around pagination & memory usage, but at least it avoids letting someone run arbitrary SQL on your database.
Proofs are actually incredibly hard to review. Problems will be found in what had been accepted to be a "good" proof years to decades later. There's a whole movement to move proofs over to something/anything more verifiable (e.g. representing all proofs in Coq--but even then you're relying on the Coq proof assistant to have zero bugs).
Furthermore, the standard for mathematical proof has also changed over time, most significantly in the early 20th century. This led to a number of existing results needing to be re-proved (or thrown out! Some were incorrect!).
Exactly what qualifies as a proof is a FASCINATING debate. Mathematics is created by consensus, just like all other knowledge.
I disagree. Phone encryption should ideally be open source-able and it's security should rely as entirely on a device specific key as possible.
I think this makes more sense for a secret project (e.x. the next iPhone), but honestly as a security person it seems overkill for anything outside national security responsible code, like state sponsored malware.
I also find it strange that the code is apparently somehow accessible outside that building (see the fired comment). If this was anything beyond security theatre, it'd be on an airgapped network and that wouldn't even be a concern (as the employee wouldn't be able to access the code from their laptop). Seems excessive for very little gain.
Yeah, which is hosted on Azure, a data center that Microsoft owns and employs guards for, and secured behind our standard corporate authentication. :) (Source: I work at Microsoft, near the VSTS team.)
It's definitely true that Meltdown is a more immediate problem--but Spectre is basically the problem that will last. We can move kernel memory into another process space, take the perf hit, and correct most of the meltdown problems.
Spectre style issues had JS pulling browser process memory using timing--the patches being "put every page in its own process" (Chrome) and "don't let people get accurate timings" (Firefox). They are way worse in the grand scheme of things, because even if they aren't as easy to exploit, they will continue to show up, probably for the foreseeable future (next 5-10 years), long after Meltdown is patched and old news.
I'd disagree as far as your position on the word "gender"--I think actually "race" is a much better example of something that has had many meanings over the course of its lifetime in the language, and isn't necessarily well defined even now.
Gender as a term that relates to people, and not words (as in the sense of the gender of a noun in Latin-family languages), has been pretty well defined since it was introduced in the 1950s--specifically as a way to differentiate between biological sex (male, female, intersex, etc.) and the social roles that people play that may or may not actually be related to biological sex (men/women/boy/girl/etc.). It's always been quite well defined, although some people feel that it either doesn't make sense to differentiate between biological sex and gender (e.x. because, perhaps, they believe that social gender roles are innate conditions of biological sex).
> But, the whole of his complaint rests on this deficiency. It's not possible to constructively disagree with someone who is unwilling to acknowledge basic facts, or who promotes an alternate reality.
This really needs to be emphasized--if you cannot agree on what the facts are, you will never come to a real conclusion. This is something the article completely glosses over. However, I also I think there's also something beneath just agreeing on what constitutes facts that is equally important, which is a (roughly) shared value system.
The old, "liberally educated" world that the author references the death of in the 1960s (i.e. "Closing of the American Mind") was one of shared values--largely white, protestant values. What replaced it was a different value system--I've seen it called the "meritocratic" value system, or similar--which had fundamentally different core values, and was/is dominant among American conservatives and liberals until recently.
Currently, the furthest left and furthest right often don't agree on core values. On the left, I think almost any argument that uses a variation on "(holy text) said so" can be dismissed off-hand as an unconvincing argument when you're talking about things beyond your own personal behavior--however, my Mormon relatives feel quite differently. This gets uglier and further away from the mainstream when you start to dig into some of the belief systems that groups on the alt-right propose (simplifying, but often things like "only white people have intrinsic value"), as opposed to the mainstream belief systems of the last ~40 years ("all people have intrinsic value"). Similarly on the far left, I've seen a lot of disagreement with other things that I'd hold up as mainstream values of the last 40 years (such as "competition between independent actors leads to good outcomes for consumers*").
Disagreements when fundamental values differ will put any argument on hold before it gets started, and I expect the only real outcome is things that devolve into shouting matches, or worse. And from what I've seen, the range of acceptable values has widened dramatically in the last 15 years--I'm curious to see if this winds up coalescing into a new set of mainstream values after a while, or if things like the structure of the internet/"filter bubbles"/increased ideological splits will mark the end of an ideological "mainstream" as it used to exist.
Late response, but: coq has the optional verification that you're proposing. :)
In my experience, Coq is not significantly harder than OCaml to write unverified code in. It's missing some nice shorthand syntax, but other than that it feels pretty similar.
With coq, the main challenge is expressing things that are meant to "run forever" (any truly unbounded recursion)--but my understanding is that would be forced to halt when it ran out of ether (so it's bounded anyways, and if you needed to you could probably explicitly hand that fact to the compiler)--and I think you probably don't want something to loop indefinitely if each iteration costs ether.
The main issues with coq that I think you'd crop up against are things that a good optimizer/compiler could probably help with (e.x. things like the fact that integers are naively represented as cons cells, so addition is O(n) and multiplication is worse). However, I haven't written any smart contracts, so it's definitely possible I'm missing something obvious.
I'd agree, and the article basically says the same thing--the language is too expressive, and therefore hard to analyze. I don't know that much about the Ether devs, but I'd expect it just didn't occur to them--even among PL folks, knowledge & experience with something like coq is somewhat rare unless you went to the right undergrad or grad school. Especially if you weren't keeping up with the latest research in the last ~5-10 years or so.
Something like Coq with a few primitives to represent interacting with the Ether network, and an optimizing, verified cross compiler would have been a perfect fit for this sort of thing, in my opinion. It's a shame that they didn't go that route, the extra dev time to get it right probably wouldn't have been equivalent to 200+ dev-years of cost (~31 million).
> We're not even close to a world where tools can offer amazing protection.
Actually, we're reasonably close--the tools aren't quite there yet for mass consumption (many are still feel quite researchy), but given that the trend of (research -> industry) usually takes 10-25 years, I'd expect that more and more critical systems will be formally verified in 10 years. Even now, companies like Amazon are using some formal methods (modelling with TLA+) to validate that specifications will behave as expected. (https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...)
Formal methods & dependent types allow for some very cool tricks on top of that--basically, you can encode in the type system a proof that the program implementation matches a specification. CompCert is a mostly-formally verified C compiler--since it was released, iirc, no bugs have been found in the verified portion of the compiler. (CompCert page: http://compcert.inria.fr/man/manual001.html)
You can also prove that the specification has particular properties (in a distributed system, things like liveness and partition tolerance). Consider the Verdi framework (allows formal verification of distributed protocols) and their formal verification of RAFT. (Code here: https://github.com/uwplse/verdi-raft)
However--it's just that it currently takes a lot more work in terms of person-hours to do the development. But formal methods are getting used in more and more places, and they do make a difference in practice. (Wired has a not particularly deep, but straightforward article that shows another use: https://www.wired.com/2016/09/computer-scientists-close-perf... )
Anecdotally, as far as effort--I'm an industry programmer who writes mostly C#. I had to learn Coq (a formally verified language) for a class--it took me a couple of simple assignments to get the idea of how it worked. Even after a few months, hacking together a formally verified interpreter for a very simple language (functions, while loops, etc.--simple, but not trivial) took about 3-4 times longer than it would have taken me to do normally.
So it turns out you can basically use type theory to encode a surprisingly large number of desirable traits about your program. (Caveat being that as you get more restrictive, you reject more "good" programs at compile time--no free lunch with Rice's theorem.)
It turns out you can encode a lot of other interesting properties in a type system (esp. if you're building on top of the existing type system), though--you can ensure that a java program has no null-dereference checks (https://checkerframework.org/ has a system that does this), and Coq uses its type system to ensure that every program halts (as a consequence, though, it isn't actually Turing complete).
There's also cool things like Lackwit (http://ieeexplore.ieee.org/document/610284/) which basically (ab)used type inference algorithms to answer questions about a program ("does this pointer ever alias?", etc.).
I'll have to watch this later, but I'd argue the issue, at least for me, isn't really surface level understanding. (At least, the kind I think could plausibly be imparted in 4 minutes. :))
The basic idea of deep learning has always seemed straightforward to me[0]. However, at least my perception is that it feels like there's a lot of deep magic going on in the details at the level that Google/Microsoft/Amazon/researchers are doing deep learning. That's honestly true of most active research areas[1], but since those results are also the results that keep getting a lot of attention, the "it's a black box" feeling makes sense to me. :)
[0] Having done both some moderately high level math and having a CS background, I feel like most ideas in CS fit this description, though. Our devil is the details.
[1] For instance: fairly recent results in weird applications of type theory are also super cool, and require some serious wizardry, but those get much less attention. (And are, I think, more taken for granted, since who doesn't understand a type system? /s)
> I'm getting kind of sick of this "deep learning is a black box" trope, because it's really not true anymore.
That's fair/probably true.
I think there's two things that drive that--one, lack of a widely shared deep understanding of the field[0] (and not really needing a deep understanding to get good results--as both you and the author pointed out), and two, the fact that it feels like cheating, compared to the old ways of doing things. :P
[0] When the advice on getting a basic understanding is "read a textbook, then read the last 5 years of papers so that you aren't hopelessly behind", there just isn't going to be widespread understanding.
I think you're kind of missing the author's point.
> My feeling is that the "perfect" abstraction of reality to geometry is actually a very high order function that we don't fully understand.
You don't need a perfect abstraction of reality, though. All you need to do is get close enough to catch up with humans or outperform them and you've solved most of the hard problems in computer vision. Fortunately--at human scales, which are the only ones you need to care about for computer vision, reality behaves closely enough to a pure Euclidean space that you're fine. :)
The author's primary argument seems slightly more nuanced, too, than just "It'd be nice if we could use old techniques".
Basically, they're claiming that if you can build geometric understanding into the ML model, you will get significantly better results that just naively plugging and chugging away with raw data. That's an empirical claim that can be validated by researchers--either it will give a significantly improved performance on well defined problems (stereo vision, etc.) or it won't. Vision is one of the research areas that have developed pretty good benchmarks over the years. :)
You get other advantages for doing three/five node replication--online updates are free if you require (n-1) compatibility.
Reality is that if you need to hit 5+ nines and require strong consistency guarantees (like "we never lose our customer's data") at data center scale, you'll probably need something similar. Most people probably don't need those guarantees, however.