electronvolt

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 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.

Yeah, all I was really saying was that the grandparent's comment and the parent's comment weren't in opposition.

Microsoft owns the data center the code lives in and certainly takes care of physical security.

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).