Viewing profile — emih

I like the story in the article, but I think it tries to create some drama where there isn't any. I think it's great that a lot of work is done using proof assistants, because clea…

Mathematically it's quite pretty, and it gives you elegant partial application for free (at least if you want to partially apply the first N arguments).

I didn't know Standard ML, that's interesting. And yeah I think this is the way to go. For higher-order functions like map it feels too elegant not to write it in a curried style.

Those are nice examples, thanks. I was imagining you might achieve this optimization by inlining the function. So if you have getClosest(points, p) = findInTree(buildTree(points), …

That's a very good point, I never thought really about how this relates to the execution model & graph reduction and such. Do you have an example of a function where this can make …

Glad to hear the article did what I meant for it to do :) And yes, another comment mentioned that Scala supports this syntax!

It's not that serious :)

You can still do this though: let result = (barbalyze(c, d, $) . foobinade(a, b, $)) input Or if you prefer left-to-right: let result = input |> foobinade(a, b, $) |> barbalyze(c, …

Thanks for sharing, interesting to see that people writing functional languages also experience the same issues in practice. And they give some reasons I didn't think about.

That's a fair point, they are all isomorphic. The distinction is mostly semantic so you could say they are the same. But I thought it makes sense to emphasize that the former is a …

Machine learning is definitely enabling writing _proofs_ within a proof assistant, and I'm sure it will help to make formal verification more viable in the future. Where it cannot …

Graph coloring is NP-hard so it would be very difficult to replace it with an O(1) algorithm. If you mean graph coloring restricted to planar graphs, yes it can always be done with…

You can't just put words in the author's mouth. It's also not true at all. For instance, teaching in primary school is a field that is dominated by women where I live, and I (and I…

The Boost algorithm computes the vertex-biconnected components rather than the edge-biconnected components, which are two different but related concepts. Articulation points are al…

That one is intentional. Note: a tree edge (u, v) is a bridge if and only if low[v] is strictly greater than the entry time of u. Here 4 is the entry time of that node. (For conven…

Whoops, you got me. Fixed! At some point I relabeled the vertices to match the DFS order, but I must have forgotten to update this example.

I used to get annoyed by these kinds of questions, but honestly I love talking about things I'm passionate about anyway and I want to get more people interested in the subject. So,…

Basically you get a bunch of problems (ranging from "check if a number is prime" to complicated graph theoretical problems) and some time to figure them out and code a correct & ef…