mafribe

30 ms·

301.
by mafribe 10y ago
Can't wait ... what kind of JIT is it? Tracing? Meta-Tracing?
302.
by mafribe 10y ago
The argument works against any language feature, not just generics. As a aside, why not add HKTs straight with generics? The problem the Go implementors have with generics seem to be about run-time representation (boxing or unboxed), but
303.
by mafribe 10y ago
More precisely, Taiwan is well connected by direct cables to Japan, China, Philippines, Viet Nam, Malaysia, Thailand, Korea, Singapore and the US. As far as I'm aware Google owns a cable connecting Taiwan with Japan (part of [1]). [1]
304.
by mafribe 10y ago
The compiler does not appear to be open at this point. Anybody know when this will change? Which team in Google is writing the compiler?
305.
by mafribe 10y ago
Many countries have a serious lack of qualified IT high-school teachers. Depending on where you live, it might be easy to branch into teaching this way.
306.
by mafribe 10y ago
The problem with verifying realistic compilers is scale. We have known how to do it in principle since forever, and verification of toy compilers is part of textbooks on verification, such as [1], see also [2]. Realistic compilers are very
307.
by mafribe 10y ago
Summary: CakeML is the first verified optimising compiler that bootstraps. Side note: Cake stands for CAmbridge KEnt, which is where (most of) CakeML's verification was carried out. The pioneering project in this space was X. Leroy&#x2
308.
by mafribe 10y ago
You can generate code for all type combinations for a and b. This will blow-up compiled code. It's a classic space-time trade-off. Moreover, you can carry out heavy static analysis that can often narrow down the possible types for a an
309.
by mafribe 10y ago
However, the JIT compilation process itself is expensive, as is the interpretation and tracing. Since JIT-optimisation happens at run-time, often sub-optimal but fast optimisations are chosen (e.g. linear scan register alloc instead of grap
310.
by mafribe 10y ago
Ocaml is a good choice, and Anil Madhavapeddy used it for his unikernel ideas. But Ocaml doesn't have strong backing any more. JaneStreet alone isn't enough.
311.
by mafribe 10y ago
Go is the language in the LXC, Docker, containerisation space.
312.
by mafribe 10y ago
Certification of weight sensors for general aviation OTOH ...
313.
by mafribe 10y ago
indicating the causal links between From the article you cite: "If the results hold up in humans ..." What reason do we have to believe that questions of free will are transferable from the mouse model to humans?
314.
by mafribe 10y ago
If anything, they're more there than they are in traditional music. Exactly. What makes modern classical music so disturbing to those socialised on pop music is the absence of endless repetition that is the true essence o
315.
by mafribe 10y ago
It's the same if you talk about seeing structures in old terrestrial tv noise patterns. Noise has plenty of patterns and structure, but it doesn't get repeated. Similar with modern classical music.
316.
by mafribe 10y ago
Modern pop music is to music what brutalism is to architecture. Cheap, repetitive, horrible.
317.
by mafribe 10y ago
it's a particular 16th note Every pop music genre has a signature sound. This is acoustic branding. It's vital for pop-music to function that the audience can determine in a fraction of a second what brand is being offere
318.
by mafribe 10y ago
As a cultural innovation, trap music is cool. In what sense? It's same old same old "Where da hoes at where da bitches at" soft-porn junk that the distraction industry has been selling to teenagers for about 3 decade
319.
by mafribe 10y ago
Where did Szilard write this? If you had a reference, I'd be grateful. Research funding was easier a century ago: https://dirnagl.com/2014/01/14/otto-warburgs-research-grant/
320.
by mafribe 10y ago
Sorted: 1582-10-04 ES Spain 1582-10-04 IT Italy 1582-10-04 PL Poland 1582-10-04 PT Portugal 1582-12-09 FR France 1582-12-14 BE Belgium 1582-12-14 LU Luxembourg 1582-12-14 NL Netherlands 1583-10-05 AT Au
321.
by mafribe 10y ago
Interesting. Could you point me towards an accessible and up-to-date description of this? I've been telling my compiler students that internally modern x86 commands are translated to RISC. I need to update my course material.
322.
by mafribe 10y ago
What verification tools would you like to see?
323.
by mafribe 10y ago
You can't have 0% corporate tax and free healthcare and education. Sure you can. You tax more elsewhere, e.g. higher VAT, higher income tax, higher captial gains, higher giraffe tax ... The possibilities are infinite. Taxa
324.
by mafribe 10y ago
C++ and Java are not even paraconsistent: every type is inhabited.
325.
by mafribe 10y ago
It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.
326.
by mafribe 10y ago
Sorry, I mean inconsistent where I wrote sound.
327.
by mafribe 10y ago
Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.
328.
by mafribe 10y ago
unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.
329.
by mafribe 10y ago
Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means in
330.
by mafribe 10y ago
MetaOCaml is about run-time meta-programming. There's your key difference.

More ›