microarchitect

Something a lot of bitcoiners don't seem to realize: the security of a blockchain is entirely due to the fact that it is too expensive to attack it. If your blockchain is "secured" by a motley bunch of ragtag microcontrollers, the first guy to point an ASIC at this chain can 51% attack it willy-nilly and render the blockchain useless.

PS. This is not a theoretical statement. It has happened to numerous altcoins.

PPS. In case it needs spelling out, the fact that its too expensive to attack the blockchain means that it is even more expensive to secure it (because miners need to make a profit).

How good is the compiler? To paraphrase David Patterson, its easy to get really great IPC for code from a shitty compiler, but that doesn't mean your program will run faster.

It's definitely colonialism and the effect of modern western media.

I know this because I grew up seeing this change happen in India. Today in India everyone (obviously an unfair generalization but still) wants to conform to the white standards of beauty. This wasn't always the case. In south india, I gradually saw the change happen; each generation of film actors was more light-skinned than their predecessors.

And if you read the classics of Indian literature, a lot of the protagonists are dark skinned. The funny thing is even a lot of the Indian gods and mythological characters are portrayed as being dark skinned in the myths, but modern paintings, TV serials and movies portray these characters with light-skinned actors!

I'm not sure if I understand what you mean by accuracy. This is not a probabilistic analysis. The solver considers the space of all possible outcomes for each match and returns satisfiable if there is some set of outcomes that satisfies the constraints. For example, it says that Stoke City can still qualify for the CL, but this requires that all of the current top 4 will need to pretty much lose every match while the teams below them win every match. This is obviously so unlikely to happen that you might as well disregard it it, but it is still a mathematical possibility and so the solver returns satisfiable.

As far as la liga is concerned, yes, you can definitely do a similar analysis. You will have to change the code that calculates the league positions, because in la liga if two teams are level on points then the first tie-breaker is head to head record, and then goal difference if the head to head is also equal. This should be a pretty straightforward change.

Honestly, 8/16b ints in C and C++ are just a minefield of problems.

Here's a snippet from an open source 8051 simulator that I was debugging today:

        if( ((RAM[ACC] & 0xF0) >> 4) > 9 || 
            GetBit(RAM[PSW], CY) == 0x01 ) {
            tempAdd = RAM[ACC] + 0x60;
            RAM[ACC] = tempAdd;
            if( ((unsigned char*)&tempAdd)[1] != 0 ) {
                SetBit(RAM[PSW], CY);
            }
        }

The code is supposed to set the carry flag when RAM[ACC] + 0x60 overflows into two bytes. Can you spot the bug? It involves my favorite C++ feature: implicit conversions, and my second favorite feature: signed chars.

The bug is that when RAM[ACC] is something like 0xFF, it gets cast to (int) -1 so the the upper byte and hence the carry flag never get set.

I predict there's lots more more evil that can milked from this fount.

I am not the OP, but I'm using Z3 in my research to help with the formal verification of hardware and firmware.

My problem is as follows. I have a microcontroller which runs firmware. I want to verify various things about the hardware+firmware combination. For instance, I may be interested in proving that user mode firmware cannot change the MMU configuration.

There are many parts to this problem. First is verifying that the kernel doesn't expose routines that let you do these kinds of things. This is a kind of s/w verification problem, somewhat well studied. Second, you want to make sure there are no h/w bugs in the microcontroller itself which the user mode software can exploit to do bad stuff. This is traditional h/w verification, also well-studied. The third is that there aren't weird corners of the microcontroller ISA specification itself which can be exploited. This is also a kind of h/w bug albeit a specification bug.

The third part is where Z3 comes in because often, there isn't any specification, and if there is, it's a bunch of PDFs or word documents. What we want is to generate a formal specification, which you can examine using formal tools to prove that it satisfies certain properties. And then we want to prove that our implementation conforms to this specification. We're using some techniques from program synthesis with Z3 as the solver for this.

This is the #1 reason why I won't stay in the US after my phd. I have no interest in being a random CEO whim away from either having to uproot my life and move back home or frantically try to land a new job all in the short period of 15 days.

For those curious the #2 reason is that H1Bs make it hard to do even simple extracurricular activities like writing books or do consulting on the side related to an open source project you contribute to let alone start a company.

The H1B is fundamentally broken and I'm amazed that so many people put up with it. Credit to the US for being such a desirable destination, I guess.

You have way too much time on your hands if you are considering review requests from people you don't know.

I was in Bangalore some weeks ago and I tried the query "OK google, directions to vidyarthi bhavan." And it worked perfectly. I was amazed!

The first thing that amazed me was that Google understood what I meant by vidyarthi bhavan! Note vidyarthi bhavan is a generic phrase in many Indian languages which just means 'student building.' In Bangalore, it refers to a specific restaurant in Gandhi Bazar famed for its masala dosas. And I bet there are plenty of people who live in Bangalore right now and don't know about this restaurant. The contextual knowledge here is amazing. And it wasn't just geolocation, I was about 15km away from Gandhi Bazar at that point. And Bangaloreans will know corresponds to an eternity given the traffic situation. And the software did all this by recognizing a phrase consisting of two words, both of which are not in English!

That moment was an epiphany for me, it the precise moment that I realized that personal digital assistants are here, and they actually work.