this is very interesting but I have a question, while the originals can't be under copyright, do the scans have a different copyright as kind of a derived work?
Verification does not need to be an all of nothing approach. Having one part of a system verified means that you are sure certain bugs can't appear on that code. So, there are less bugs in total, and when facing such a bug you know where you don't need to look.
Otherwise you never end, you have to verify your code, the compiler, the operating system, the processor, quantum physics, the creator of the universe...
In my case I think it is after "a lot of sifting through academic language" that I get a cool idea through my thick skull. Academic language is (or should be) about being precise not obscure.
What I am trying to say, is that learning takes time. The simple, no nonsense terms resonate in your mind after you really grasp the concept. Otherwise it's just a high level overview that won't allow you to really use the concept.
The article kind of confuses hacker as in "Linus Torvalds is a hacker", and hacker as in "Kevin Mitnick is hacker". While I don't think the word cracker will ever be popular, at least we should not mix the concepts.
It's a national development fund controlled by the president, not his personal bank account. It is suggested by analysts that Chavez uses the money as his way to "buy elections" (probably by subsidizing the poor, and not helping the "trickle down" economy by giving the money to the rich). Of course some money gets lost, it always does, right or left goverment.
3rd criteria can be considered a vulnerability, it may allow to know that certain user has a known file. It can be exploited to reveal information about the encrypted files.
They've set an example on how to do a peaceful revolution. They've earned the right to choose their own government.
Now, they'll have to learn from their choices, good and bad ones!
Chromium still uses a gnu make based build system. He did this "for fun" to investigate a potentially faster way. I am very envious, my "for fun" activities never result in something so cool.
I don't think it's crazy. As someone already said the objections are probably related to the examples mentioned on the book (election results and other "controversial" subjects).
Crazy is superficial, this is, in my opinion, sad but not crazy or stupid.
I wrote a small compiler for a 'haskell' called HNH with type inference that generates C code, with a small runtime including GC. Everything is done very naively, but it's a hugely interesting excercise.
You can find it in https://github.com/fferreira/hnh