fmap

14 ms·

151.
by fmap 10y ago
The most alarming thing is that they are explicitly cutting anything to do with climate change (there's a more comprehensive overview here: https://www.washingtonpost.com/graphics/politics/trump-presi... ). Th
152.
by fmap 10y ago
Do you have any particularly memorable example of a complicated proof which was lacking complicated "trivial" details? My experience (I work in interactive theorem proving) is that many such proofs are subtly wrong.
153.
by fmap 10y ago
As others have already pointed out, this has been tried before. Turns out that some people are opposed to shipping LLVM with the browser, or any other large existing codebase. The reality is that WASM has to target the existing JavaScript b
154.
by fmap 10y ago
I just looked at a few of the problems and these are really well designed. From what I've seen, there's always a clear progression and a way to get partial credit. Plus the problems themselves are interesting and non-obvious. So h
155.
by fmap 10y ago
This is wonderful, can't wait to use it for my own code. :) Though at the moment the semantics isn't entirely clear to me. For instance, in the protocol example, shouldn't the pair be using multiplicative linear conjunction?
156.
by fmap 10y ago
That's a relief. All the OCaml that I've seen has been a horrible mess of single character identifiers without comments or type annotations...
157.
by fmap 10y ago
I've tried to read academic papers on E Ink displays before and the slow refresh times have always been a dealbreaker. On the other hand, I just read the advertisement for ReMarkable and made a note to buy one when it comes out... A ge
158.
by fmap 10y ago
Yes, that's what I had in mind. Another thing I seem to recall is that Turbofan used to be a lot slower than Crankshaft and spend a lot of its time in scheduling and register allocation. Has this changed recently? In any case, I'm
159.
by fmap 10y ago
What do you mean exactly? Grothendieck universes correspond to the some inaccessible cardinals, but the axiom that every set is contained in a Grothendieck universe (which is stronger than just saying that there are omega-many inaccessible
160.
by fmap 10y ago
Can you link to some of the references you cite? That seems like an interesting read. As for computability being a physical notion, I can't speak to the motivation of Church and his students, but I do know that there are characterizati
161.
by fmap 10y ago
Finally! Congratulations to the V8 team for completing the switch to a sane compilation pipeline. :) Hopefully this will lead to many more simplifications in the future. Does anyone know which optimizations finally catapulted Ignition+Turbo
162.
by fmap 10y ago
There is a lot of ordinary mathematics that is outside of ZFC, which Friedman is well aware of but the writer of this article may not be. Grothendieck was not interested in abstract set theory when he introduced what are now called "Gr
163.
by fmap 10y ago
Sheaf models are one of the most useful tools in logic and I'll definitely read this paper once I have more time again. One thing that seems strange to me based on the overview video is the focus on sheafs on a topological space. In ma
164.
by fmap 10y ago
Who "choose" OO 20 years ago and (much more importantly) why? I'm going to ignore the social component... that said, we work in a wonderful profession where the world is changing completely every decade and many design deci
165.
by fmap 10y ago
This looks impressive, but does anybody know why "exact coverage" is apparently considered the gold standard for rendering vector graphics? Mathematically, computing pixel coverage corresponds to sampling a box filtered version of
166.
by fmap 10y ago
This definition is actually required for the correctness of many standard compiler optimizations such as partial redundancy elimination and code motion.
167.
by fmap 10y ago
Anything that humans can do is a priori possible. :) It is merely unlikely to happen while there is anything else left which we can't automate...
168.
by fmap 10y ago
"Reducing the number of available jobs" is a very reasonable statement. How much time do you spend gluing together ready made components? How different is the latest CRUD app you wrote from the first one you wrote? That's def
169.
by fmap 10y ago
JavaScript is JIT compiled, it has to be parsed, typechecked, interpreted and eventually compiled. WebAssembly is parsed and then translated to machine code (with a much simpler compilation pipeline). Typical JavaScript VMs have a lot of fa
170.
by fmap 10y ago
Yes, and indeed Gödel himself believed in an objective mathematical reality. What I meant to say is that the commonly accepted basis for mathematics (first order logic and ZFC) was first justified using arguments which later turned out to b
171.
by fmap 10y ago
The problem solution in the article uses the axiom of choice to construct a "nonprincipal ultrafilter" on the natural numbers. This is actually weaker than the full axiom of choice, but you can still show that no such object is co
172.
by fmap 10y ago
I think historically the Curry-Howard correspondence grew out of the observation that combinatory logic and Hilbert proofs look very similar. There does not seem to be a large overarching story that doesn't makeup some history after th
173.
by fmap 10y ago
I'm not sure if you can really cast this as a debate between Church and Turing. It is certainly a difference between Brouwerian constructivism and this presentation of the Curry-Howard isomorphism. I think you'd be much happier wi
174.
by fmap 10y ago
I agree with this personally, but if you read through VPRI's publications you will find that the vast majority of their DSLs seemed to converge to "functional with some special features (which you could implement in Haskell using
175.
by fmap 10y ago
From a reasoning perspective throwing an exception is the same as returning from a function. If you want to reason about code which potentially throws an exception you have to keep track of a separate exception post condition. If you compil
176.
by fmap 10y ago
Complexity theory abounds with such algorithms in order to solve concrete problems. In fact it's even worse than that. There is a whole subfield of complexity theory which looks for "fixed-parameter tractability" and typicall
177.
by fmap 10y ago
WebAssembly is very different from LLVM IR, because it is essentially just the greatest common denominator of what existing JavaScript VMs handle in the backend. For instance, WebAssembly allows only reducible control flow, has very limited
178.
by fmap 10y ago
I can add a few more data points. First regarding CakeML: - CakeML is written in HOL4, which is using ML. - SML, unlike Ocaml has a well-defined semantics and so there is a good starting point for a verified compiler. Second, regarding Ocam
179.
by fmap 10y ago
Well, you do get an (expected time) asymptotically efficient algorithm for sorting the first k elements of an array by running quicksort without recursing on the last n-k elements. This is what you get in Haskell with "take k (sort xs)
180.
by fmap 10y ago
This is a wonderful book and I recommend it to anybody learning Coq. The mathematical components project has made (and continues to make) great strides when it comes to formalizing research level mathematics. Before this book, there was onl

More ›