madez

How do you avoid the Intel chips in networking? Intel has often-used Ethernet and WiFi chips.

The Chinese government thinks it could lose the power struggle over Hong Kong, while it was confident about the Chinese invasion and assimilation of Tibet. Hong Kong is a real threat to the Chinese regime.

Yes, demonstration (as in presentation) effect.

I'm very excited about India's ambitions. It would not only be meaningful for India, but for many people around the world. We are lacking open chips, and project Shakti is on a trajectory to solve a part of that.

I wonder when GCC learns to use the source code of the hardware along with the source code of the software to optimize the binary with full knowledge of the system.

Which better alternatives to VHDL and Verilog do you mean?

I can't answer how much research or work is done to make the tools more user-friendly as I'm rather exclusively on the user-side. There exists extensive documentation in form of multiple PDFs, but they are only of little help to me as they lack useful examples. Sadly Google thinks every possible answer about Isabelle/HOL is answered by these PDFs as they are often the only relevant search result.

However, Isabelle/HOL/Isar allows proofs to be written in a very human readable way, so the "documentation" I use is the existing library and how things are done there. There is a convenient Ctrl+left click action on terms to jump to their definition. That is very helpful to navigate unknown libraries. In comparison, I couldn't read and make sense the proofs I've seen in Coq.

There is a learning curve with Isabelle/HOL/Isar. It can be extremely frustrating to not know how to express "simple" arguments or definition. But for someone familiar with manual "formal" proofs in mathematics, most can be learned in some hours under guidance, like in a seminar on a weekend with a couple of hours on each day.

I'm learning rather autodidactly by trial and error. I think there would be value in a series of blog posts about "This is how you define a group" or "This is how you reason in nonclassical logic" or "This is how to proof the fundamental theorem of Algebra" all applied to Isabelle/HOL/Isar. There are often multiple ways to define things, and to be honest, I don't know the specific advantages and disadvantages. For example, I think you can introduce rings as type classes or as locales or using axiomatizations, and possibly more. This is one example of stuff I don't know how to manage in the system, but there is already a lot of structure defined, and I can reuse that.

I'm currently working on the formalization of Catalan's conjecture (or Mihăilescu's theorem) in Isabelle/HOL/Isar.

My personal impression is that more formal verification is necessary in math, and it should be tought to every student of Mathematics in introductionary courses because it gives an unforgiving but also rewarding learning experience with formal proofs.

Feel free to ask questions.

It would be better to stay quiet instead of comparing things incorrectly.

We are not used to be free. Economic restraints force us to do things we don't want to do instead of watching Netflix. So most don't understand what "just watching Netflix" means. If you set out to "just watch Netflix" as your main activity, you would very very quickly get fed up and depressed, and thus stop watching Netflix.

Those fortunate ones with enough wealth to have the option to just watch Netflix for a year and don't do much else, don't do that and are happy with it. And neither would the less fortunate once after an initial learning phase. Humans must learn to be free, but they can. We want to take part, show our contribution, feel proud. As soon as we have found a pleasant way to contribute, we do.

Yes, conditionless basic income would change work ethics. People who fill up supermarkets displays or serve food to unfriendly customers at unhealthy hours would maybe just stop going to work. I would be happy for them, and I hope it would happen today.

There is a lot of work that is needlessly tiring, badly paid, and in which you are badly treated, but people just stay in the status quo because they see no way out. Once there is a way out, the jobs will have to change, and that rapidly. That would be progress for society I still hope to see in my lifetime.

> Which would you rather have? A wealthy society with inequality or a poor society without inequality?

This is a good as in goodwill and honest point here. However, I think it isn't a dichotomy based on evidence. For example, most of northern Europe has these programmes and they are not poor, and there exist many poor countries without these programmes. If I thought these programmes would leave the people less wealthy, healthy, happy, I would be against them.

If the programmes create negative incentives in people as to not be productive and successful to a degree that offsets the advantages in reduced crime, more tax because of higher educated people and thus salary and countless other and not easily measured advantages like progress on science, culture, and art, then I would be against those programmes. This is however not what we are seeing. It is a scary shadow on the wall while we can see the cute bunny in the foreground with our eyes directly.

This reads like a figurative kick in the face to those who argue against free education and social programmes "because the market will solve it and those that work hard enough will make it, so it's fair". The world is deeply unjust economically and the vast majority loses from that, and those, that manage the inquality by using the cheap larbor and forced constraints of the disadvantaged to serve the more fortunate ones, win. Even the fortunate ones win from rich neighbours, so there should be a big consensus for universal conditionless free education, social security and health insurance backed by the government.

I know this might be interpreted as a flamebait and I see the common "but the government is incompetent/corrupt/inefficient" answers already, but those don't negate what I just wrote in any way upon closer inspection. However, this is genuinely how I feel and I feel stupidified when I see how these programmes aren't yet serious international standards.

Isn't the solution introducing another type of memory abstraction in the kernel next to "available since boot" and "hot pluggable", namely "later added but won't be removed"?

But there have been reasons given. They want to use standard tools to deal with the log. They want to see the scripts that manage the system and poke around in it, which has the implicit reason to learn about the system and being able to easily modify it.

And a flag in the wind is soft and gives in. Shall we all thus be flags in the wind?

> within this theory, then begins to exist retroactively.

That is evidently what they keep the data for. They want to be able to have the data to access it eventually. If they didn't want to access it eventually, they wouldn't keep it. That is why mass collections, that are stored, are wrong.

When it is FIPS 140-2 level 4 certified, they will let you know early enough so when it's missing you can easily tell.

> Something without an management engine would certainly possible, but would be limited to niche products like the librem.

I don't share this forecast. I think many private customers would view a machine without the ME and it's capabilities as a plus for a product when the marketing is done right. Especially since most don't care for the capabilities.

Is there a Windows version for RISC-V? Can they still legally use it? Do they want to dependent on Microsoft? I think these are questions that need an answer and I doubt that they are all answered affirmatively.

Intel has a huge variety of different models. They are experts in market segmentation. They could do that. But they won't, and there are few who could do that.

With RISC-V, it is reasonable to expect multiple vendors to provide CPUs. There is a very good case to expect non-backdoored chips.

You talk negatively about the protests with broad accusations, but without bringing facts to back them up. I really wish I hadn't to counter this.

> It's immaterial in these protests as it is a manifestation of despair due to economic reality and worsening living conditions without a hope of revival.

The protest started because of the extradition law. Then, due to police brutality against the protestors, the demands widened to these areas.

I question your truthfulness. Was Hong Kong in economic despair? And is that the reason for the protest?

Also, the economy will take a hit because of the protests, so after some time there will be an effect visible. But be honest here, and don't mix up cause and symptom. Also, even if the economy of Hong Kong suffered, you have yet to show that the protests are because of that.

Furthermore, you claim there is "[no] hope of a revival". Well, if the Chinese communist regime works on making them suffer, it will be more difficult to prosper, but without that there is no reason why they shouldn't have success. It's a red flag that you make this claim.

> Extradition treaty require local competent court to make a decision whether to extradite or not. But For majority of protestors it is immaterial because the perception is that Hong Kong do not have a decent judiciary or legal system, it works at the whims of China (again a perception created by few). So the actual discussion no one wants to discuss or hear.

Edward Snowden went initially to Hong Kong because of the high independence and quality of their court system.

I want to hear discussion, after all I'm here because of that, but I don't want to hear echoed propaganda.

Your third point is an attack on the protestors. The AfD in Germany did something like that at a demonstration of children for measures against climate change. They asked them highly specific question regarding the actual percentage of CO2 in the air. Most got them wrong, and the AfD used that to devalue the protestors and the protest.

It is obviously clear that you do not need to understand the details to have a valid political demand that you can voice in a demonstration and protests. Insinuating otherwise is another red flag.

Can you even acknowledge a single demand the protestors are making?

Are all accesses to the memory from the GPU still checked for permissions at the hardware level by an IOMMU?

It's not like they are bad people who set out in the morning to make the world a worse place. If you want change, you must question what makes people behave that way. The extreme focus on economic success of individuals combined with a lack of solid social security is what my intuition tells me drives people to do things at work that damage other people. Is there research about this?

It isn't an argument on the topic and it isn't supposed to be. It is a reminder for you to stay rational and avoid ad hominems.

Nuclear reactors in cars are a bad idea. Even if they can be built small and never needed refueling, cars get destroyed in all imaginable ways all the time, so the nuclear pollution would need to be expected to be released often. Also, we don't have a solution for the contaminated waste that millions of nuclear powered cars would produce.

We can satisfy our power needs from renewable sources with existing technology to competitive prices.

I cannot get the game to play correctly. I'm using Debian with AMD open graphics, and about everything works fine, but this game is horribly broken with it. I'd love to play it.

It seems you are inutitively always converting everything to the decimal system and taking that as "the way" to think about numbers. That wouldn't be surprising, because we are brought up this way and even our language focusses on the decimal system. Not having good words to speak about the binary number 1101001 makes it difficult to think about it without converting it first. Two (I'm decimal again!) isn't a good base for human communication because there is a lot of repitition of simple symbols. Maybe a new way to pronounce hex numbers like a17c03 would be able to replace the decimal system.

I have seen a lot of very good indie games in some genres, but not in all. Can you point to some good indie realtime strategy games?

I was also once called out by dang. He did it so respectingly and understandingly that it made a change for me. This was much better for my reflection about what was wrong about my behaviour than if I had been moderated more heavihandidly. I don't understand the amount of attention and patience that is necessary for it, but it makes a difference.

We are one in many. That means we just share the influence. Many issues are not binary, and often the individual contribution to a problem can be canceled out completely by individual change. The influence may be small compared to the sum of all, but still the responsibility for the individual contribution lays completely with the individual. The comparison must be between the individual cost and the individual contribution to the problem and it's solution, not falsely to the complete problem on the scale of the society.

Even when the problem is binary, the argumentative position becomes much stronger by individual change. For example, if Europe became fully carbon neutral, it's stance would be much more powerful when it comes to these questions compared to if it continued to build new coal power plants and told other countries to stop doing that.

I do not advocate individual change as a tool to rely on to solve problems, so this is a straw man. That would disregard other effective and efficient ways to approach problems. I also don't think it's about "personal ethical edification". That is again a rather condescending spin you are giving to it.

My point is about recognizing the individual influence one has. Often that is avoided by the statement I'm criticizing.