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 you definitely want to architect your…
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 backtrack, so boolean formulae (ie, SAT)…
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 the only constant was his hatred of…
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 things more difficult for those not…
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/interesting. So he asked a historian…
"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 taking ideas seriously, and so to honor…
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 a gift of similar value at some point…
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 program transforms a stream of inputs into a…
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 in the 1990s. Really! In the first…
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 very attractive ideology -- if the worst…
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 recursively decrement the reference counts…
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 French mathematicians in the 1920s and…
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 big and exciting enough to be worth 2…
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 about it. Like, I have enough money to…
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 course Gauss-Jordan would show up there.…
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 Eliot had to say about Judaism in After…
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 CPU has an instruction cache and a data…
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 agents can have a budget in balance, be in…
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 more likely, as hard) as ordinary math.…
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 about Pratt parsing since it is a special…
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 is Vickers' Topology via Logic, from…
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 algorithms is Valiant's algorithm, which is…
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, you can describe it as a state machine,…
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 the popularity of antivax ideas on the…
Willie Wong wrote a nice blog post about this a while ago: https://williewong.wordpress.com/2010/03/18/compactness-part...
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 you definitely want to architect your…
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 backtrack, so boolean formulae (ie, SAT)…
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 the only constant was his hatred of…
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 things more difficult for those not…
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/interesting. So he asked a historian…
"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 taking ideas seriously, and so to honor…
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 a gift of similar value at some point…
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 program transforms a stream of inputs into a…
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 in the 1990s. Really! In the first…
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 very attractive ideology -- if the worst…
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 recursively decrement the reference counts…
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 French mathematicians in the 1920s and…
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 big and exciting enough to be worth 2…
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 about it. Like, I have enough money to…
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 course Gauss-Jordan would show up there.…
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 Eliot had to say about Judaism in After…
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 CPU has an instruction cache and a data…
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 agents can have a budget in balance, be in…
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 more likely, as hard) as ordinary math.…
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 about Pratt parsing since it is a special…
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 is Vickers' Topology via Logic, from…
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 algorithms is Valiant's algorithm, which is…
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, you can describe it as a state machine,…
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 the popularity of antivax ideas on the…
Willie Wong wrote a nice blog post about this a while ago: https://williewong.wordpress.com/2010/03/18/compactness-part...