more_original

11 ms·

61.
by more_original 11y ago
> To be precise it's not our ID cards that we like to microwave but our (travel) passports. No, this article is about ID cards. The new ID cards, introduced a few years ago, also have RFID chips. https://en.wikipedia.org&
62.
by more_original 11y ago
"Don't worry about people stealing an idea. If it's original, you will have to ram it down their throats." -- Howard H. Aiken The real difficulty seems to be to distinguish between ideas that genuinely deserve rejection
63.
by more_original 11y ago
"Effective Java" by Joshua Bloch is very good.
64.
by more_original 11y ago
"Don't worry about people stealing an idea. If it's original, you will have to ram it down their throats." -- Howard H. Aiken
65.
by more_original 11y ago
I'm not sure that's the case in Munich. There are special arrangements for exchange students, but it seems that everyone else is treated in the same way. For university accommodation there are waiting lists for various buildings,
66.
by more_original 11y ago
> By the way only 280€ in Munich seems a little off to me... Yes, it's more to the tune of 500€ at average for a room in a shared appartment (Source: https://www.wg-suche.de/magazin/wg-zimmer-preise-an-hochschu.
67.
by more_original 11y ago
The differences weren't that great. German has a number of distinctive dialects (Bavarian, Saxonian, etc.), and with Saxony in the east, there have been historical differences anyway. The Saxonian dialect has sort of become synonymous
68.
by more_original 11y ago
This page is from 2006! I guess the official homepage http://ocaml.org would be better for up-to-date information.
69.
by more_original 11y ago
> The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that you've very carefully verified. That's what I mean. The LCF approach
70.
by more_original 11y ago
MLton is unsuitable for LCF-style theorem provers, simply because it has no interactive toplevel. ML was originally developed as a MetaLanguage for such theorem provers. The idea is to have an abstract type thm of theorems, whose operations
71.
by more_original 11y ago
Yes, I forgot about petrol prices, which have increased substantially. I'm not so sure about infrastructure improvements, at least here in Germany. I have been cycling for more than 20 years, and the infrastructure has not changed that
72.
by more_original 11y ago
I think you're right that this is a factor. What it doesn't quite explain is the decline of car usage in European cities that have always had sidewalks and good public transportation and where cycling isn't much easier now th
73.
by more_original 11y ago
Yes, that was poorly worded. Europe is big. I meant to say that there are places (specifically in Europe), where it's perfectly possible to go through one's whole life without a owning car and without missing out.
74.
by more_original 11y ago
You're absolutely right. I understand "peak car" as trying to get away from unreasonable car use. Like in the US where one has to use a car for trips that one could easily walk, if only there were sidewalks.
75.
by more_original 11y ago
Fair enough. What you describe sounds much like I feel about bikes. Taking the bus and train to work takes over 30 minutes, while the bike ride is just 10 minutes. Going by car would certainly take more than 10 minutes here. Someone once sa
76.
by more_original 11y ago
I live in Europe and have never even considered getting a car. In cities the bike is the fastest mode of transport anyway, and for longer distances it's quite convenient to take the train.
77.
by more_original 11y ago
> 2. What happened in Germany in ~1975 that made them suddenly start working? I think it may have been the oil crisis in 1973. During the crisis, industry did not have enough work for its workforce. Instead of mass-layoffs, they tried to
78.
by more_original 11y ago
Similar story here. Our parents made sure that all children could swim well as early as possible. I remember them supervising us only as long as there was a weak swimmer in the group. From then on I think they generally kept an eye on where
79.
by more_original 12y ago
There's also the T450.
80.
by more_original 12y ago
> Isn't this just socialism? No. "Socialism is a social and economic system characterised by social ownership of the means of production and co-operative management of the economy, [...]" http://en.wikipedia.org
81.
by more_original 12y ago
I'm German and I'm happy to pay taxes. You do get something for everyone in return (infrastructure, education, some social security (which has been eroded, unfortunately), health care, etc). Also, I studied in the UK and my tuitio
82.
by more_original 12y ago
> Go also forced me to write readable code: the language makes it impossible to think something like “hey, the >8=3 operator in this obscure paper on ouroboromorphic sapphotriplets could save me 10 lines of code, I’d better include it
83.
by more_original 12y ago
Oh, but they're already building a verified Coq compiler: http://www.cs.princeton.edu/~appel/certicoq/
84.
by more_original 12y ago
> If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. We're verifying the compiler from one language to the other. The specific
85.
by more_original 12y ago
Yes, that's a valid point. The idea is to first give a high-level formalisation of the C language definition and then to prove that the compiler correctly implements this. In the case of CompCert, the specification is given by a big-st
86.
by more_original 12y ago
The proof is written in Coq, an automatic proof checker. Of course, Coq itself could have bugs, but it has a small trusted kernel and it produces proof objects that can be checked, so what you get is much, much more reliable than the typica
87.
by more_original 12y ago
Also merlin is worth mentioning explicitly. It finds and highlights errors during editing (in emacs, vim and co), does autocompletion, shows types and since recently can also write pattern matches automatically. http://the-lambda
88.
by more_original 12y ago
You can extract lazy values that represent infinite data. For example, you can define the stream of the factorial numbers as follows. CoInductive Stream (T: Type): Type := Cons: T -> Stream T -> Stream T. Fixpoint fac(n : n
89.
by more_original 12y ago
I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
90.
by more_original 12y ago
Yes, one can represent non-terminating programs. One can represent Turing machines as data, after all. But one cannot write a Coq function that will fully execute such programs. Each well-typed Coq function, when applied to concrete argumen

More ›