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…
"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…
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…
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…
This note represents a rare misstep by Dijkstra: the pigeonhole principle actually is a special and important principle worthy of a special name of its own. For example: 1. When you formulate the pigeonhole principle in…
See Ken Ishii's music video "Space Invaders 2003": https://www.youtube.com/watch?v=p--dHQIeagE It's super cute, and also hits like a truck. Detroit techno is a really inspired musical choice for this kind of thing.
Vector spaces and linear maps between them form a model of the linearly-typed lambda calculus. That is, each type can be interpreted as a vector space, with each well-typed term representing a linear map between vector…
Gap buffers are zippers, which makes this particular case really easy: they arise as derivatives of the list functor, and so for generic categorical reasons they are isomorphic to a list plus a position in it. This…
Well, this was an utterly nonsensical waste of time. A much wiser and more humane attitude towards continental philosophy was expressed by the great analytic philosopher Michael Dummett, who remarked that the division…
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…
"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…
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…
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…
This note represents a rare misstep by Dijkstra: the pigeonhole principle actually is a special and important principle worthy of a special name of its own. For example: 1. When you formulate the pigeonhole principle in…
See Ken Ishii's music video "Space Invaders 2003": https://www.youtube.com/watch?v=p--dHQIeagE It's super cute, and also hits like a truck. Detroit techno is a really inspired musical choice for this kind of thing.
Vector spaces and linear maps between them form a model of the linearly-typed lambda calculus. That is, each type can be interpreted as a vector space, with each well-typed term representing a linear map between vector…
Gap buffers are zippers, which makes this particular case really easy: they arise as derivatives of the list functor, and so for generic categorical reasons they are isomorphic to a list plus a position in it. This…
Well, this was an utterly nonsensical waste of time. A much wiser and more humane attitude towards continental philosophy was expressed by the great analytic philosopher Michael Dummett, who remarked that the division…