more_original

13 ms·

91.
by more_original 12y ago
In Coq all functions terminate. Coq's correctness depends on termination. In Coq the propositions are types. To prove a proposition is to construct a program of this type. If one allowed non-termination, then it would be easy to cons
92.
by more_original 12y ago
Reminds me of Hoare's quote on ALGOL 60: "Here is a language so far ahead of its time that it was not only an improvement on its predecessors but also on nearly all its successors."
93.
by more_original 12y ago
This sounds like a really interesting idea. I probably takes a weekend to prepare a proper application anyway, so spending the time on a project (which may be fun even) sounds much better.
94.
by more_original 12y ago
> I honestly think this is ridiculous. Sure, this is an incredible feat, and congrats. It's not that bad (or difficult), really. It's a hand-written parser for a subset of C that emits assembly code right away. This is how comp
95.
by more_original 12y ago
> I'm also pretty sure that the compiler is extremely limited in what it can do here. And that is dangerous, as running in constant space is often a matter of correctness, not one of optimization. I would rather have the compiler e
96.
by more_original 12y ago
Maybe you could have a look at "Unix system programming in OCaml"? http://ocamlunix.forge.ocamlcore.org/
97.
by more_original 12y ago
> Berlin, Pre-War: https://www.youtube.com/watch?v=B-m9A8mY-U0 Some scenes are also from Munich. Around 3:00 you can see Odeonsplatz, for example. It pretty much looks the same today ;).
98.
by more_original 12y ago
CP/M/3.1 (Pentium (like 386); Intel AMD) DOS 6.0 Windows/6.4 (NT, like Mac OS X) Windows/95 Windows/10
99.
by more_original 12y ago
I haven't read the immutability patent in detail, but it seems like the problem they are considering is not completely trivial. I've seen research papers on similar topics. Example: http://www.cs.ru.nl/E.Poll/
100.
by more_original 13y ago
Have you considered using some standard library replacement like Core?
101.
by more_original 13y ago
I think one reason the Pumping Lemma is emphasized so much is that it is a good exercise in logic . We often find that students have difficulties with quantifier alternations (there exists x, such that for all y, there exists z, such that.
102.
by more_original 13y ago
Right, and we should hold them to their own standards. If they have the capacity to do all this surveillance, then I sure as hell expect that they know exactly who the email addresses they're passing on belong to. And they should be re
103.
by more_original 13y ago
Yes, that's my point. We shouldn't say that most people use X because it doesn't seem clear cut at this point.
104.
by more_original 13y ago
I'm not sure it is right to speak of "most people". Many people use OCaml these days. For instance, I have the impression that in work on program verification and static analysis OCaml is more popular than Haskell. Coq is wri
105.
by more_original 13y ago
But we don't actually know for sure that this is what happened, right? At this point it seems to be just speculation that is being repeated as hearsay.
106.
by more_original 13y ago
Or maybe **C, to account for all the indirection.
107.
by more_original 13y ago
You need to know the type. I wouldn't want to say that makes reading code "hard", but it means that you need more context in order to understand the code. (Imagine, for example, that you're trying to understand a patch, where not all types
108.
by more_original 13y ago
Yes, it's verbose, but verbosity also adds information that may be useful (although + is probably not a good example for this). With 'easier to understand' I mean that when looking at a bit of code I can tell what it does without having to
109.
by more_original 13y ago
Actually, I also think that Haskell will not become mainstream. As a matter of fact, one of the main things I do not like about Haskell is that the type class mechanism makes too many things implicit and that it allows too much overloading.
110.
by more_original 13y ago
I think there are philosophical reasons why people prefer inference rules over working with sets. Many people work or have worked in a context of constructive logic, as constructivism comes in naturally when you consider computability. Now,
111.
by more_original 13y ago
The inference rule notation is standard within mathematical logic, which is where it comes from. I'm not an expert on the history of mathematics, but I've seen inference rules for example in Gentzen's 1935 paper and I'm sure they are quite
112.
by more_original 14y ago
Something similar happens to me. When I'm really exhausted from the day, I fall asleep while reading or relaxing (maybe from 9pm to 2am) and then wake up again. I'm then awake and do a few things for an hour or two. I like how it messes wit
113.
by more_original 14y ago
Yes exactly! I always find it really impressive that ML and its type inference were developed in the 70s, only just a few years after C had been defined.
114.
by more_original 14y ago
Yes, commercial use is allowed, but the LGPL requires attribution. The site you give does link prominently to the LGPL license.
115.
by more_original 14y ago
This is my experience exactly. Cars are generally predictable and most drivers are really careful. In my experience most dangerous situations arise from pedestrians walking on te cycle lane abruptly or from other cyclists that don't obey th
116.
by more_original 14y ago
Please substantiate. An attacker knowing an internal collision of the hash algorithm for m1 and m2 (of the same size...) can construct HMAC(m2,key) from HMAC(m1,key) without knowing the key?
117.
by more_original 14y ago
Well, if you have an internal collision hash(m1)=hash(m2) and both messages m1 and m2 are of the same size, then it seems that one would also get hash(m1|key|size) = hash(m2|key|size). So, I cannot really see how appending the size will hel
118.
by more_original 14y ago
For example, if you already happen to know a collision hash(m1)=hash(m2), where m1 and m2 have full block size, then you also get a collision hash(m1|key)=hash(m2|key), just as explained in the article. So, one could forge messages, which s
119.
by more_original 14y ago
RFC 2104 specifies how you should do it, see e.g. http://de.wikipedia.org/wiki/Keyed-Hash_Message_Authenticati... The Handbook of Applied Cryptography, Chapter 9 (free online: http://cacr.uwaterloo.ca/hac/ ) nicely explains the reasons.
120.
by more_original 14y ago
> > The way to really understand the idea is to re-create what the author left out. > If reading mathematics requires re-creating what the author left out, why not leave it in? To really get some feeling for the content of the t

More ›