mafribe

46 ms·

421.
by mafribe 10y ago
Do you mean Huaca Pucllana by any chance?
422.
by mafribe 10y ago
I'm not sure what you mean. We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main difference is that HOL-based provers like Isabelle/HOL has classical built in from the start -- all proof aut
423.
by mafribe 10y ago
I'd say, we up the difficulty of our discussions. Things we would discuss in the past (e.g. which year was XYZ born) are now settled beyond dispute with a quick google. Now we are stuck discussing questions that cannot be resolved this
424.
by mafribe 10y ago
Most of the rest of the world seems to go the other way: voice calls are rare and reserved for emergencies, SMS has been replaced by WeChat, WhatsApp, LINE and the like, and a data-only phone would be much more useful to most than a voice o
425.
by mafribe 10y ago
Yes, I agree, the shift from reading to writing is pronounced, and probably profound. After the Internet went mainstream, for the first time in history, large number of people write every day, people who wouldn't have, in comparable so
426.
by mafribe 10y ago
I was reflecting on this the other day. How do we communicate now? What are the key features of how we communicate that were not available before. Maybe it's the combination of the following. 1. Written, using language++ (by this I mea
427.
by mafribe 10y ago
Do you know what kinds of optimisations Erlang/BEAM does for clusters of independent nodes? Does the user have to tell Erlang/BEAM which thread lives on what node, or does the scheduler handle this automatically?
428.
by mafribe 10y ago
It might be helpful to be a bit more precise here. The expression "first-order logic" (FOL) is a bit vague. Do you mean pure FOL (i.e. all axioms are about equality) or FOL plus additional axioms? Pure FOL (without additional ax
429.
by mafribe 10y ago
That is true, but does proof automation work as well for classical reasoning in Coq as it does in Isabelle/HOL where classical reasoning is 'baked in' from the start? As far as I'm aware, the question of moving the &quot
430.
by mafribe 10y ago
I'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in
431.
by mafribe 10y ago
Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/
432.
by mafribe 10y ago
This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL and Coq).
433.
by mafribe 10y ago
The short answer is yes. That's because (1) a classical system like HOL can use external automatic theorem provers ("sledgehammer") that are based on classical logic (most of them are), in a way that constructive systems like
434.
by mafribe 10y ago
A crucial question for fast execution of the BEAM-machine on multiple cores is how expensive message copying between cores is. With that many cores, there's probably no shared memory between all cores. How do the remaining cores commun
435.
by mafribe 10y ago
If, a comparatively similar amount of effort and research would have gone into developing cures and treatments for the other diseases, the benefits would have also been, probably, order of magnitudes greater. I
436.
by mafribe 10y ago
This is just nonsensical. The main reason why the Spanish were successful was political: the Incas (which means "rulers") had forged their empire with violence and the tribes they subjugated were only too happy to get rid of the I
437.
by mafribe 10y ago
ISIS have neither popular support nor superior weaponry? Are you sure? ISIS is supported by Saudi Arabia and Qatar (who are probably money laundering fronts for certain other states that shall remain anonymous). Pizarro had one cannon, and
438.
by mafribe 10y ago
One feels that there is a certain ... tension between your That cannot be accepted as an 'axiom' without proof. and your Proving this is nearly impossible
439.
by mafribe 10y ago
I was not addressing the question of whether the axioms are true or not, although I have an opinion on this matter. I was addressing lazy "whataboutism". You still have not given an workable account of what you would accept as &qu
440.
by mafribe 10y ago
Yes I do. Let's not forget that ISIS almost managed to take over Syria and Irak, what makes you think they would not take over France if the French let them? A hand full of socialist revolutionaries took over Russia, and ruled for near
441.
by mafribe 10y ago
how do we know similar acts did not take place?? We are pretty sure that many pre-democratic changes of political power did come about in this way. Revolutions and other political power-struggles have been studied very careful
442.
by mafribe 10y ago
Exactly what would you accept as proof? A deduction in ZFC or Homotopy Type Theory? Or an empirical experiment, where we split the world into two parts, one were we police terrorism as the french are doing now, and one where terrorists are
443.
by mafribe 10y ago
no significant mortality risk to Europeans. This is "Whataboutism". The rational behind being wary about terrorism is as follows. 1. Normal homicides are random individual actions, and they are under reasonable control by
444.
by mafribe 10y ago
That means BEAM - Pony is not a fair comparison, because cooperative schedulers solve a much simpler algorithmic problem.
445.
by mafribe 10y ago
Ohhh that would be amazing, have you got inside information that you can share?
446.
by mafribe 10y ago
Thanks, that's interesting. Linear types are useful, undoubtably because they can reduce copying. What kind of scheduling does Pony use?
447.
by mafribe 10y ago
Where does Pony's performance vis-a-vis Erlang/BEAM come from? The absence of dynamic typing? Better scheduler?
448.
by mafribe 10y ago
Another problem with 1ML is that it's only a research prototype for now, so we can't take it "for a spin". Given the 1ML inventor's main job, this is unlikely to change any time soon, unless some kind soul takes on
449.
by mafribe 10y ago
provide just let polymorphism and ML-style type inference I mostly agree with this, and this should be the default starting point for any new programming language. If B. Eich had built Javascript on this basis, the world would
450.
by mafribe 10y ago
This is orthogonal to parametric polymorphism Higher-rank types are not orthogonal to parametric polymorphism, instead they are a special case. You can see this when you realise that rank-k polymorphism is a subsystem of System

More ›