mafribe

20 ms·

151.
by mafribe 9y ago
Asian nations have done drastically worse to each other Coincidentally, this is true of Africa as well: Mengistu Haile Mariam, Mobuto Sese Seko, Idi Amin, Samuel Doe, or the Tutsi/Hutu conflict were typically much more vi
152.
by mafribe 9y ago
Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle : https://wwwbroy.in.tum.de/~berghofe/papers/TYPES
153.
by mafribe 9y ago
the value of the property increases over time Is this a law of nature?
154.
by mafribe 9y ago
“I cannot answer for them what they are going to do with the quadratic equation. I don’t know why they are learning it.” If Mr Rochelle cannot answer this question, and recommends just googling it, he might not be a
155.
by mafribe 9y ago
I'm not saying this can't be done, au contraire! Indeed cost coherent programming idioms can be converted into typed language primitives. But there is a price to pay in terms of typing system complexity. It's a slippery slop
156.
by mafribe 9y ago
Destructors seem to be a pain point The problem is not so much typing as such (things that don't return anything but terminate -- as destructors do -- can be typed as Unit) but rather to find a good trade-off between ex
157.
by mafribe 9y ago
Wouldn't that be a good path: start with initial experiments based on types-by-macros, and see how well that works. Can't be worse that C++'s template meta-programming.
158.
by mafribe 9y ago
I agree. I wonder if Rust's compile-time meta-programming can be used to implement 'pluggable' linear-types for experiments, maybe along the lines of [1]. That might be a good compromise. [1] S. Chang, A. Knauth, B. Greenman,
159.
by mafribe 9y ago
Such questions are best answered after MLoC or GLoCs have been written.
160.
by mafribe 9y ago
As a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types. How does that fit Probably doesn't and typing
161.
by mafribe 9y ago
arguing against The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmat
162.
by mafribe 9y ago
LOL, thanks. That's a great suggestion. Next time I'm teaching compilers, I'll illustrate the difference between context-free and context-sensitive language with reference to Glasgow pubs.
163.
by mafribe 9y ago
isn't about their appearance Pro-tip for the socially savvy: intuit what about their appearance they put a lot of though/effort into, and then make a compliment based on that. Examples. - Your new hairstyle is amazing, wh
164.
by mafribe 9y ago
Previous discussion https://news.ycombinator.com/item?id=13963858
165.
by mafribe 9y ago
I would argue that Islam is currently undergoing it's reformation: to Wahabism. Its printing press is the internet. And it's the best funded reformation imaginable, all that oil money goes towards spreading a variant of Islam that
166.
by mafribe 9y ago
Demand exceeds supply
167.
by mafribe 9y ago
there is only so much land There is way more land than needed, if only we build cities dense enough. Have a look at e.g. Hong Kong's density: The Kwun Tong district in HK has 57250 persons per square kilometre [1] which, assu
168.
by mafribe 9y ago
Universe means: model of set theory. Goedel's incompleteness theorems guarantee the existence of non-standard models of set theory (and Peano arithmetic). Hamkins cleverly uses non-standard models to construct a single program that ca
169.
by mafribe 9y ago
Interesting. I'm not familiar with the Californian model. But as with direct democracy in cities and villages, California is not a country, so certain life/death decisions, like engaging in warfare, are not applicable. Moreover,
170.
by mafribe 9y ago
Direct democracy is dangerous. So are all other forms of governance. The only significant example of direct democracy in action has been Switzerland, and it's been pretty successful in comparison. Yes, n=1 is not good, but be
171.
by mafribe 9y ago
Exactly why are you suggesting that US senators are a credible source of information in this matter? US senators have also said that there are weapons of mass destruction in Iraq, and that Assad used chemical weapons against the Syrian popu
172.
by mafribe 9y ago
That's why the Russians hacked Macro What is your evidence that this hack originated in Russia?
173.
by mafribe 9y ago
Agreed. Wikileaks has a sterling record regarding the authenticity of their own leaks. Given that the Atlantic Council is for all practical purposes an arm of the US government, and it's "Digital Forensic Research Lab" is ext
174.
by mafribe 9y ago
TLDR: - Post goes out of its way not to deny authenticity of the leak. - Post can be traced to the Atlantic Council [1]. [1] The Atlantic Council (AC) is a core ingredient for US soft power [2] projection on other countries. Example membe
175.
by mafribe 9y ago
If you worry about accreditation and brand recognition, why not do a Bachelor's degree in Europe for free/cheap and then do a Masters in the US? The Masters programs in top US universities are much easier to get into than their u
176.
by mafribe 9y ago
You can, but Berlin is not (yet) where most of the interesting high-tech jobs are. Moreover, if you want an interesting social life, eventually you'll have to learn the local language, there's no way around it.
177.
by mafribe 9y ago
Where are those highly paid tech jobs in the UK? Apart form a bit of fin-tech in London, most programming jobs in the UK are quite badly paid and not comparable with US/SV salary levels. I see what my UK-based students are earning, and
178.
by mafribe 9y ago
Have you considered using the "Facebook News Feed Eradicator"? It does what the name suggests it does, and let's you focus on events and private messages.
179.
by mafribe 9y ago
The prime purpose of CT is unification, showing that many familiar things are instances of the same idea. In that sense CT is shallow, you can always in principle do without CT what you can do with. But without the abstract view afforded by
180.
by mafribe 9y ago
No, g is given by a ↦ f (e a a). The expansion you refer to works because e a0 = g.

More ›