Viewing profile — neel_k

I do software verification. In my experience, Z3 is consistently but noticeably better than CVC5 at the kinds of problems we generate, though the two tools are close enough that yo…

If you have a bound on the size of the largest type in your program, then HM type inference is linear in the size of the program text. The intuition is that you never need to backt…

Richard Rorty, whose humanism and love of democracy MacIntyre despised. Over the course of his career, MacIntyre went from an extreme left Marxist to an extreme right Thomist, and …

Let's translate your comment from scientific research to driving: > If driving on the road suddenly makes car trips possible, then I'd say that the road is indeed designed to make …

You are reacting to the title, not the actual article. 1. The author is a CS professor who wanted to make a "CS for non-majors" course that non-majors would find actually useful/in…

"On Inequality" is one of the very worst pieces of serious analytic philosophy I have ever read. The best part of Franfurt's intellectual tradition -- analytic philosophy -- is tak…

Actually, there are very similar situations in Chinese culture! My understanding is that when someone gives you a gift, in Chinese culture there is a social obligation to give them…

Surprisingly, FRP doesn't have anything to do with dataflow constraints at all. In FRP, a program is fundamentally a function of type Stream Input → Stream Output. That is, a progr…

Luckily, lawyers in the 1970s already figured this out, by anticipating the research on causality that computer scientists and mathematicians like Judea Pearl and Peter Spirtes did…

This is really easy to explain: all of the colonial empires were horrifying engines of atrocity, oppression and death. Since imperial apologists hated socialism, that made it a ver…

The short answer is: reference counting walks the dead part of the heap, and tracing gc walks the live part of the heap. When a reference count of an object goes to zero, you recur…

It's worth understanding the context Bourbaki arose in. An entire generation of French mathematicians was turned to bits of blood and gristle in the trenches of World War I, and so…

When I went to one of these things, it was pretty much entirely about how to scope the work and how to write the proposal. Eg, for a big ERC grant, you need to propose something bi…

Same way that I (who left industry to pursue an academic career because I wasn't happy) cope with the feeling I am missing out on a giant FAANG salary: mostly, I just don't think a…

It sort of depends upon the course. This particular syllabus looks like a really standard linear algebra course (I have no idea what is robotics-specific about it), and so of cours…

Of course Eliot was a great poet, but the impulse to hagiography is one that should be resisted, and despite a gesture at that fact this article mostly fails to do so. Here's what …

Self-modifying code was useful for optimisation back in the 80s, but these days it's usually awful for performance (with JIT compilation as the main exception to this rule). Your C…

Sure it can. Actual competitive markets are made of competing firms, and firms can't (in general) optimise. 1. Holmstrom's theorem tells us that no payment system for a team of age…

For behavioural correctness of terminating functional programs, you can by and large treat your programs as plain mathematical functions. Then reasoning about them is as easy (or m…

Pratt parsing (aka top-down operator precedence) is a special case of LR parsing. Since Laurie Tratt (the author of the article) is advocating LR parsing, he has no need to talk ab…

Do you mean topology, or geometry? For topology, there are two main constructive approaches. The first, better-developed one, can be found in the theory of locales. An easy intro i…

In the conclusion, raph writes: > I am even more convinced than before that efficient parsing is possible on GPU. IMO, the place to start looking for GPU-friendly parsing algorithm…

Basically, it doesn't. TLA+ is first-order temporal logic, where you can write formulas describing how the state of a system evolves over time. If you have a concurrent process, yo…

Nowadays anti-vaccinantion is substantially a marker for being on the right, since Donald Trump ran for president while making anti-vaccination claims. This tremendously increased …

Willie Wong wrote a nice blog post about this a while ago: https://williewong.wordpress.com/2010/03/18/compactness-part...