jbapple

33 ms·

271.
Verified Lisp implementations on ARM, x86 and PowerPC(cl.cam.ac.uk)
1 points by jbapple 16y ago|0 comments
272.
Who Verifies the Verifiers?(blog.regehr.org)
12 points by jbapple 16y ago|0 comments
273.
by jbapple 16y ago
> I suspect people laughed at him, told him he would never succeed, told him he should do other things. I don't think that's true. IIRC, Wiles was pretty successful before he started the work (tenure at Princeton?), worked on it secretl
274.
by jbapple 16y ago
> For any given Haskell Compiler I would think that I can construct a program where the Haskell Compiler won't be able to determine, in polynomial time, whether the list has length 0 or not. Ok, sure, but in total languages (that is, la
275.
by jbapple 16y ago
> If the Epigram is not Turing complete, then what kind of programs cannot be expressed in it? I think one quick answer for questions like this is "an interpreter for $LANGUAGE". The reason is that, for a language in which all programs
276.
by jbapple 16y ago
> when your program compiles it will be guaranteed to behave correctly This is only true if you give your program a strong enough type, and giving your program a stronger type may make it harder to write. For instance, here is a 14-line
277.
by jbapple 16y ago
> It is impossible to ensure that a monad within Haskell conforms to the monadic axioms (in other words, it is impossible to ensure a monad within Haskell is actually a monad). It is impossible to ensure almost anything in any programmi
278.
by jbapple 16y ago
> When you tell someone "this is a O(logn) operation" they do expect log performance. If you look in the appendix of your algorithms textbook that explains big-O notation, you will see this is not the actual definition. I'm sorry if my
279.
by jbapple 16y ago
> I get the feeling these can do things Random Access Lists can't It seems like you came to this topic without knowing a lot about purely functional data structures already. It's good to learn and explore new things, but from this comme
280.
by jbapple 16y ago
> Which function on assoc lists is O(log n)? acons is O(1), and the O() notation is for upper bounds, so anything O(1) is also O(lg n).
281.
by jbapple 16y ago
> trellises require Omega(lg n) for cons. In the worst-case, I mean.
282.
by jbapple 16y ago
> How are these better than balanced binary trees that keep subtree size in the node? I suspect that cons will be )(1) amortized (when the trellis is used ephemerally), which is not true of your usual balanced binary trees. There are ma
283.
by jbapple 16y ago
> I know this is a big claim Perhaps, but it needn't be to get the same asymptotic performance. Okasaki's simplest random access list has performance proofs that depend only on the simplest properties of binary numbers, rather than thos
284.
by jbapple 16y ago
> How do these differ and what advantage do they offer over Chris Okasaki's Random Access Lists? These are inferior, as Okasaki's structure offers O(1) worst-case cons, even when used in a functional setting. As far as I can tell from t
285.
by jbapple 16y ago
> of those composite data types (which also includes assoc-lists and...?), it is the only one with O(logn) for any of its functions (particularly search). I think you meant "all", not "any", since assoc list offers O(lg n) performance f
286.
by jbapple 16y ago
When I first saw a "proof" like this, the explanation of its incorrectness was something like "limits don't preserve curve length". I wasn't satisfied with that answer until I took a first course in real analysis, which explained (some of)
287.
by jbapple 16y ago
KERMIT said: "Are you sure about that? I've seen co-workers suggest the use of Coq, only to see a room full of managers and peers burst out in laughter." I think my claim that "People who 'specialize in this language' generally work in a fi
288.
by jbapple 16y ago
maxklein said: "I'd never specialise in this language because everyone will turn to a teenager when you are listing your skills." Coq is not a general-purpose programming language. People who "specialize in this language" generally work in
289.
by jbapple 16y ago
pascal_cuoq said: "There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of computer-assisted proofs." For predicates that can be computed in coq, we can do aw
290.
by jbapple 17y ago
> He could a bigger loon than she is, it takes two to make a fight. He could be, but we have no evidence of that. Furthermore, she admits sending the messages. It does not "take two" to make an assault.
291.
by jbapple 17y ago
> I don't get why Sean C.'s version is more believable than Diane Goodman's FTA: "Over the next few hours, she sent several more angry messages. She warned of a 'world of pain.' 'Goodbye pussy boy I will be contacting your employers,' s
292.
by jbapple 17y ago
Here is a list of features that Yeti has that are either not in Python or not in Algol. That is, none of these features is in both Algol-60 and Python: * static typing * discriminated unions * first-class functions * immutability by default
293.
by jbapple 17y ago
Regarding the last question: "what happens with yeti when you have polymorphism and mutable containers?" In section: http://linux.ee/~mzz/yeti/intro.html#type-declarations "Variable (and argument) bindings are not polymorphic (it would ma
294.
by jbapple 17y ago
Here is another way to run an ML-like language on the JVM: http://ocamljava.x9c.fr/ It supports all of OCaml, but it seems complicated to get running along Java with the same sophistication as Yeti. For instance, it seems that one must us
295.
by jbapple 17y ago
I would teach them about quicksort and mergesort. Little known fact: most of the technological stagnation of the dark ages was time wasted in bubblesort.