Viewing profile — 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…

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 me…

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…

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 subse…

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 li…

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…

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 take…

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 …

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,…

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 …

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 …

> 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 a…

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 missi…

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…

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

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 …

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 minu…

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

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 …

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 …

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 …

Having experienced slight feelings of melange/detachment following novels, video games, and movies in the past, and having experienced what this article is describing: it's not qui…

"If it ain't broke, don't fix it." goes for attacks, too. Why spend weeks/months searching for 0-days and hoping they will remain viable when you can spin up a fake login page and …

> here are at last 3 obvious approaches: (1) applying the functions sequentially, (2) concatenating their outputs, (3) XORing their outputs. None of these takes rocket science to f…

> I don't know when you read my comment, but I edited it (I think) some ~15 minutes before you posted your comment to clarify that I wasn't referring to stacking arbitrary hashes. …