doall

Kawakami has been deeply concerned about the declining Japanese animation industry. Since he has been involved with Studio Ghibli and Studio Khara he knows the industry quite well. Also as CTO of Dwango he knows quite well about technology and the open sourcing stuff could be done only by him.

Bravo Kawakami!

I am already aware of the Barr Group team and I know their claim.

>NASA didn't find a software defect, this is not the same as NASA finding that there is no software defect.

Read my post carefully. I haven't claimed such a thing and I offered two possibilities.

>Toyota absolutely built and sold dangerous vehicles with software and hardware defects.

You have to be careful with this. The Barr Group team haven't proven the relationship between the accident, and the software defect which they claim to found of.

The important thing is that software, hardware, system, and the whole design for car safety can improve significantly better than the current situation, which is much more better than just relying on human drivings.

About the Toyota's unintended acceleration (UA) incidents. From Wikipedia: "On February 8, 2011, the NHTSA, in collaboration with NASA, released its findings into the investigation on the Toyota drive-by-wire throttle system. After a 10-month search, NASA and NHTSA scientists found no electronic defect in Toyota vehicles.[27] Driver error or pedal misapplication was found responsible for most of the incidents.[28] The report ended stating, "Our conclusion is Toyota's problems were mechanical, not electrical." This included sticking accelerator pedals, and pedals caught under floor mats.[29]"

https://en.wikipedia.org/wiki/2009%E2%80%9311_Toyota_vehicle...

If this was true, then the self-driving car may have prevented the accidents. If it was really a software problem, then fix the software. It may be much more easy to fix the software rather than to fix human behaviors.

That is very true and thanks for telling from the other side. Hope that Koreans and Japanese will get along.

A typical Japanese will not hate a person because of having a Korean ancestry. Actually there are many celebrities who have a korean background and also are very respected.(e.g. Masayoshi Son, Akiko Wada, Tomoaki Kanemoto, Akira Maeda)

Typically, Japanese people are kind and generous, and they will closely look at the person's attitudes. The people who are not liked are the people who hate Japan and the Japanese people.

As an example, people who graduated from the Korean School (Chousengakkou) will be given an Anti-Japanese education. I heard from a Korean background person that at a Korean School, if you speak Japanese at the school, you will be beaten by your mates.

Few years ago, there were K-POP trend in Japan, and people were very interested in Korean culture and the Korean people. But when they start knowing that the majority of Korean people have huge hatred towards Japan and also the Japanese people, now many Japanese people are becoming suspicious when they hear the word Korea. It is not because they are racist or not. It is just a rule of thumb or statistics.

See this https://groups.google.com/d/msg/homotopytypetheory/oXQe5u_Mm...

>all mathematical proofs are actually programs

This is not true. Only a subset is stated by Curry-Howard correspondence.

First of all, thank you for changing the license to BSD. This is a really happy news. Reading all the discussions including Google Group, HN, and Reddit so far, to deal with the concerns of hga and others, is it possible to just move the comment part of the licence.pdf to porting.htm? Perhaps the main motivation of the changes to BSD was to encourage shenturions and potential shenturions to use Shen at work, and we are almost there. If you do that, then nobody will claim the licence, and we can move forward. We don't want to see anymore hatred just because of the licence issue. We want to focus on developing real applications using Shen at work and see the Land of Shen to expand. Please consider if you think this is reasonable. Thanks

Shen's powerful T* type system using sequent calculus which is turing complete is revolutionary.

Also, Shen's approach doesn't have a huge performance hit. See benchmarks for Qi implemented in SBCL. http://www.lambdassociates.org/studies/study10.htm