mafribe

85 ms·

781.
by mafribe 11y ago
I agree that there is scope for JITing in Haskell. But JITing is not without cost, and in statically typed languages, some of the big gains that make JITs for Javascript or Python so powerful, go away. If you are using C in a way that requi
782.
by mafribe 11y ago
The JVM is not a tracing JIT compiler. Tracing is a very slow operation. Hence the warmup problem is substantially worse for tracing JITs. I saw figures for warmup in tracing JITs that were so hillariously bad, that I thought they must b
783.
by mafribe 11y ago
The Schilling paper is mostly a re-rendering of the original paper Dynamo: A Transparent Dynamic Optimization System [1] by Bala et al, which invented (or better reinvented and popularised) tracing JIT compilation. It might be worth
784.
by mafribe 11y ago
As far as I'm aware partial evaluation JITs like Graal/Truffle have atrociously bad warmup times. Warmup is the phase before the optimised code is ready to be executed. This is already a problem for tracing JITs, but is supposedly
785.
by mafribe 11y ago
Most young feminists oppose alimony, Where are all those young feminists campaigning against alimony, for 50/50 shared custody in divorce, equally severe sentencing criminal cases for men and women, draft for women, etc? I&#
786.
by mafribe 11y ago
I'm a man and have spoken with many other feminists over the years, and read a lot of feminist literature, philosophy, cultural criticism, etc. In my experience I'd say that more than 99% of feminism/feminists have all to do
787.
by mafribe 11y ago
If you hike at altitude, say above 3.5 km, you'll encounter few animals and plants. The Andes in Peru, Bolivia and Chile are very suitable for this kind of hiking. The sun is even stronger than at sea level though!
788.
by mafribe 11y ago
Typo should be: ... differentiation is a binary ...
789.
by mafribe 11y ago
I didn't want to convey the impression that social differentiation isn't a binary, either/or process. Differentiation has been going on for millenia with some setbacks along the way.
790.
by mafribe 11y ago
There are also real, documented, movement for men's rights, for example fathers rights organisations. the fact that you'd make that comparison is, I think, extremely telling. Could one not argue that it is telling us that
791.
by mafribe 11y ago
"The road to hell is paved with good intentions".
792.
by mafribe 11y ago
CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) and computes the characteristic formula (expressed in the logic of Coq) of th
793.
by mafribe 11y ago
The Cold War basically prevented some internal conflict within the Communist Bloc by providing an external menace and scapegoat. That's an interesting theory, but I'm not sure I can agree with it. Before the Sino-Soviet
794.
by mafribe 11y ago
realizing the abstraction of a unified Communist block was pretty faulty, and national interests superseded any ideological fidelity to the Communist cause. Interesting perspective. I think sino-soviet split, which was ideological
795.
by mafribe 11y ago
As another counterfactual to build intuition: had the KMT beaten Mao in the 1940's, would there be a Communist Vietnam? Moscow sent weapons to Ho Chi Minh's and Pol Pot's armies via China. So it's extremely do
796.
by mafribe 11y ago
Exactly. Korea itself of course has been dealing with communists. Burma and Laos had communist insurgencies. The CP of Laos, too, is an offshoot of the Vietnamese CP. Most of Africa and South America had strong communist parties too. It&#x2
797.
by mafribe 11y ago
In what sense was it hot air? Saloth Sar (better known as Pol Pot), radicalised by the French communist party, trained in Moscow, Belgrade and Beijing, took over neighbouring Cambodia, aided by the communists in Hanoi. Indeed the Cambodian
798.
by mafribe 11y ago
I'm not 100% sure what your question is, maybe you can clarify? The evolution of society from the stone ages to modernity is characterised by increasing: 1. Functional differentiation. That means we specialise more in smaller and small
799.
by mafribe 11y ago
Most (all?) three- and four-letter abbreviations are already used. Context disambiguates.
800.
by mafribe 11y ago
CFML stands for "Characteristic Formulae for ML". Characteristic formulae are a powerful concept of program logic. Simplifying a great deal, given a program M, a characteristic formula for M is a pair (A, B) of logical formula suc
801.
by mafribe 11y ago
"It's used for ritual/religious purposes" is an archaeologist's polite way of saying "we don't know what it's for, but it was probably central to the rulers of society". The strict functional di
802.
by mafribe 11y ago
"You have to be willing to blow things up in order to be effective in negotiating strategy." Y. Varoufakis on "Behind the news" podcast, 2014. Varoufakis is using classic populist rhetoric: - Simplisitc notion of the ca
803.
by mafribe 11y ago
Very nice descriptions. While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble. Let's say we have a formula A which is classically and constructively t
804.
by mafribe 11y ago
No. Classically, LEM and double negation are equivalent. Intuitionistically the situation is more complicated, see the discussion in this thread by IngoBlechschmid: We can prove that LEM implies double negation, but not the other way around
805.
by mafribe 11y ago
I don't think synthetic homotopy type theory is known to cover all of conventional homotopy theory, so it's work in progress.
806.
by mafribe 11y ago
A proof in mathematics is not purely syntactic because it's not purely logical. This is confusing constructive reasoning with the decision problem for proof validity. They are different things. The very point of logic, constr
807.
by mafribe 11y ago
While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural
808.
by mafribe 11y ago
Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers. You need to distinguish betw
809.
by mafribe 11y ago
j2kun's characterisation of HoTT is misleading. Their goal is also to rewrite all of mathematics in a constructive way, This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive.
810.
by mafribe 11y ago
Typing systems (at least some of them) are also logics. This is called the Curry-Howard correspondence (CHC). At first the CHC was made to work for propositional logic only, i.e. logic without for-all and existential quantification. Later

More ›