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 you definitely want to architect your verification tool to be able to use either one (or both at once, in case you hit a problem which is pathological in one but not the other).

One place where Z3 exposes a superior interface to CVC5 is when you want to do term simplification. CVC5 does not have any real analogue to Z3's simplification tactics (like ctx-solver-simplify), so if you want to take a term and simplify it with respect to a set of assumptions, Z3 is your only choice. I think CVC5 has all the machinery you need to implement that stuff inside of it, but as a user you can't access it.

The place where CVC5 really pulls ahead of Z3 is when you want to produce proofs (eg, to integrate SMT solving into a proof assistant like Lean, HOL, or Rocq). Both tools have support for generating proofs, but CVC5's are noticeably less buggy, to the point that Lean's SMT integration uses CVC5, even though Leo de Moura (Lean's designer) was also the original designer of Z3.

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) offer no help in expressing the type inference problem. That is, if you think of HM as generating a set of constraints, then what HM type inference is doing is producing a conjunction of equality constraints which you then solve using the unification algorithm.

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 liberalism. He really couldn't stand the idea that people could believe in rationalism, feel the moral force of individual rights, or make purpose and meaning for themselves, all without appealing to an authoritarian source of control.

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 driving on the road.

This is obviously silly, because the road makes car travel easier, not harder. Schemes like Horizon Europe make scientific research easier in similar ways.

For funding agencies to give money to universities, they and the univerisities have to make a whole bunch of critical but basically arbitrary decisions about how to handle the impedance mismatch between their respective organisations' internal finance procedures. Doing this over and over is wasteful of time and effort, and one benefit of big cross-national research funds like this is that a university can make these decisions once, and then don't have to do it over and over again, once for each funding agency in Europe.

Also, generous cooperation is an important part of geopolitics. Cooperation is how you convince your neighbors you are an ally rather than a threat.

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 colleague what she wanted her students to know about computers.

2. She replied that she wanted her students to know that (a) databases exist, and if properly designed/indexed can make complex queries very fast, and (b) websites can be automatically populated from the results of DB queries, which makes these search results human-comprehensible.

3. In his CS department, databases and HCI/web design are courses which come late in the sequence, after stuff like algorithms, data structures, and networking.

4. To make (2) accessible without a bunch of pre-reqs, he designed an extension to Scratch/Snap (block-based visual programming languages) which let novices more easily write SQL queries and generate database-backed HTML documents.

5. As a result, he can now teach history majors CS concepts in a way which makes their relevance to historical work directly clear.

"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 his life I'll try to make a brief but serious critique of "On Inequality".

This book essentially concatenates two essays, "Economic Equality as a Moral Ideal", and "Equality and Respect". In the first essay, Frankfurt argues that economic equality is less important than the worst-off having enough. As a result, political appeals to the importance of equality are bad philosophy. In "Equality and Respect", he generalises this to a general attack on the concept of egalitarianism.

The basic problem with his work is that the social world is so incredibly abstracted that the truth value of his claims is simply irrelevant -- they have no insight to offer about our actual world. In his essay, he considers different distributions of resources, but gives no serious thought to the actual mechanics of how resources are distributed.

This is fatal to his argument because resource actual distributions are endogenous, rather than exogenous, and so they can't be compared in a vacuum -- to say something meaningful, you genuinely have to take seriously the fact that control of resources is a form of power, and that the powerful tend to use their power to reinforce and maintain their status. So politics and policy -- things he explicitly denies having anything to say about -- are fundamental to understanding the issues involved.

Even making the tiniest possible effort towards taking these issues seriously blows up his argument. For example, suppose that we have people living in a perfectly competitive market. This is about the smallest possible step towards social realism that you can possibly take!

But even here, Negishi's theorem tells us that at a Walrasian equilibrium, the implicit social welfare function maximises the sums of each person's utility, scaled by the inverse of each person's marginal utility of wealth. Now, suppose our people have a utility function which is logarithmic in their wealth -- U(w) = log(w). Then their marginal utility U'(w) = 1/w, and the inverse of that is w. That is, ideal markets value individuals linearly in proportion to their wealth. So the utility function of the ideal market says that saving Jeff Bezos's life is worth the lives of 1.2 million Americans of median wealth, 8 million Poles, or 36 million Indians.

It makes one think that Frankfurt must have used "On Bullshit" as an instruction manual when writing "On Inequality".

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 in the future. So giving a very expensive gift can be a very rude gesture, because it effectively inflicts a large, unexpected expense on the recipient.

In Western culture, there is a similar dynamic when it comes to dating and courtship. The general expectation is that men will ask the women they are interested in, and the women will then accept or refuse the offer. The difficulty with this is that it puts women in the position of having to reject someone who is 20 cm taller/20 kg heavier than them -- this can be very scary.

So it is artful/polite for a man asking a woman out, especially in the initial stages, to do so in a way that is ambiguous enough that if she decides she doesn't want to continue, she can back away without having to forcefully reject him. An overly strong confession of love removes this ambiguity, and thereby forces a woman into the uncomfortable position of having to directly reject the man. This is rude, in exactly the same way that giving someone an overly-expensive gift is rude in Chinese culture.

Naturally, though, in China very close friends wouldn't be bothered by how expensive gifts are, and that in the West, a woman pining for a particular man would be delighted if he directly declared his love for her. But we have etiquette to handle the failure cases, not the success cases!

Anyway, I'm always surprised how even though people are basically the same everywhere, and share the same desires and impulses, we end up building very different cultures. It's just amazing how situations can be radically different and utterly familiar at the same time.

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 stream of outputs. If you think about this a bit more, you realise that any implementable function has to be one whose first k outputs are determined by at most the first k inputs -- i.e., you can't look into the future. That is, these functions have to be causal.

The causality constraint implies (with a not-entirely trivial proof) that every causal stream function is equivalent to a state machine (and vice-versa) -- i.e., a current state s, and an update function f : State × Input → State × Output. You get the stream by using the update function to produce a new state and an output in response to each input. (This is an infinite-state Mealy machine for the experts.)

Note that there is no dataflow here: it's just an ordinary state machine. As a result, the GUI paradigm that traditional FRP lends itself to the best are immediate mode GUIs. (FRP can be extended to handle asynchronous events, but doing so in a way that has the right performance model is not trivial. Think about how you'd mix immediate and retained mode to get an idea about the issues.)

When I first started working on FRP I thought it had to be dataflow -- my first papers on it are actually about signals libraries like the one in the post. However, I learned that basing it on dataflow and/or incremental computation was both unnecessary and expensive. IMO, we should save that for when we really need it, but shouldn't use it by default.

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 instance, you just can't use race as a feature, since it is a protected characteristic. But, you might also be worried that protected characteristics can generally be easily identified by looking for innocuous traits that correlate (since people tend to cluster into communities). For example, if you know an American's ZIP code and their three favorite musicians, you can determine their race with an accuracy in the high 90s. (Basically, the US is still just as segregated now as it was a hundred years ago, and black and white Americans tend to listen to different music.)

So when the US Civil Rights Act was passed, the courts came up with the idea of "disparate impact" -- when doing something like hiring, you are not allowed to base the decision on features that disproportionately affect one group rather than another, even if they are formally neutral, unless the feature directly impacts the ability to do the job.

In other words, you have to show that the features you are basing the decision on _causally influence_ the decision you are making, exactly like you see in Pearl's causal influence diagrams or structural equation models or whatever. Eg, if you want to hire a math professor, you can base the decision on the articles they published in math journals, but you can't base it on whether they like old school Goa trance.

So, what about black box neural networks, where you don't know which features are being used? In this case, it's pretty clear that you shouldn't use them directly when making a home loan, because the law wants to know what features are in use, and you can't answer the question of whether you're redlining when you have a black box. However, using black box techniques to learn (eg) the best random forest model to use is fine, because it lets you easily see which factors are going into the decision before deploying it.

FWIW, people have been doing this for decades already. (I did stuff like this back in the 1990s.)

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 people alive hate something, it's got to have something to recommend it, right?

The Madras famine of 1877 (in which over 8 million people died) is characteristic. The British Empire didn't just fail to help, it actually made it illegal to offer food relief, on the grounds that it would distort the labour market and violate free-market principles. If you witnessed that, wouldn't you think the market and Moloch were one and the same?

It's worth noting that "concentration camp" is not the English translation of "Konzentrationslager": it's actually the other way around. The German word is the translation of an English phrase used to describe the British Empire's interment camps in the Boer War. IMO, it's impossible to look at, say, a picture of Lizzie van Zyl and not see a premonition of the Holocaust.

https://en.wikipedia.org/wiki/Lizzie_van_Zyl

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 of everything the object points. This leads you to trace the object graph of things whose reference count has gone to zero. You never follow pointers from anything which is live (i.e., has a refcount > 0).

When you are doing the copy phase of a gc, you start with the root set of live objects, and follow pointers from everything that is live. Since anything pointed to by a live object is live, you only follow the pointers of live objects. You never follow pointers from anything which is dead (i.e., garbage).

If object lifetimes are short, most objects will be dead, and so RC will be worse than GC. If object lifetimes are long, most objects will be live, and GC will be worse than RC.

Empirically, the overwhelming majority of objects have a very short lifetime, with only a few objects living a long time. (This is called "the generational hypothesis">) So the optimal memory allocator will GC short-lived objects and RC long-lived objects. Rust/C++ encourages you to do this manually, by stack-allocating things you think will be short-lived, and saving RC for things with an expected long lifetime.

Beyond this, RC has a few really heavy costs.

Reference counting doesn't handle cyclic memory graphs. You need to add tracing to handle those, and if you are going to do tracing anyway, it's tempting to just do tracing really well and skip the refcounts entirely.

This is because the memory overhead of reference counts is high -- empirically, most objects never have more than a single reference to them, and so using a whole word for reference counts is lot of overhead. Moreover, the need to increment/decrement reference counts is really bad for performance: first, mutations are expensive in terms of memory bandwidth (you've got to maintain cache coherence with the other CPUs), and second, in a multicore setting, you have to lock that word to ensure the updates are atomic.

There are tricks to mitigate this (e.g., Rust distinguishes Arc and Rc for objects which can be shared between threads or not), and there are schemes to optimise away RC assignments with static analysis (deferred reference counting), but if you want to do a really good job of reference counting, then you will be implementing a lot of tracing GC machinery.

And vice versa! The algorithm in the link is partly about adding RC to handle old objects (empirically, as part of the generational hypothesis, objects which have lived a long time will live a long time more). In fact, Blackburn and McKinley (two of the three authors of the above paper), pioneered the combination approach with their paper "Ulterior Reference Counting."

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 early 1930s faced an acute shortage of teachers who were current with modern mathematics.

The premise of the Bourbaki effort was to write everything down in enough detail that a sufficiently motivated reader could learn it without having to learn it master-apprentice style -- because too many potential masters were dead.

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 million euros, but small enough that you and 3 students/postdocs can do it in five years, since that's what 2 million euros can pay for. But our grant office did make sure that most of the speakers were people who had actually applied for these grants in the last round.

One really key thing for me was to reach out to senior colleagues in the same area (definitely not just at the same university) to get multiple examples of what successful grant applications look like. There's a bunch of text in the grant call, but the panel are going to be senior in-area academics who may know what a good application looks like, but won't necessarily be able to articulate all the rules.

Everyone I know finds writing proposals hard. So much of writing papers is being careful about citing prior work and not over-claiming for your results, but for grant proposals we are basically forced to make big claims about things that we have not done. However, it's worth noting that no one on the panels or at the grant agencies see research proposals as binding promises to do certain work: they mostly all want you to follow the science and change course if you spot something better.

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 afford a house and take my kids on vacation from time to time. So having lots of money is something I idly wonder about sometimes, but no critical need is going unmet by its lack.

Conversely, if you have a prestigious position, most likely everyone around you does too. For example, I'm a professor, and yes, it makes my mom proud. But all of my colleagues and many of my friends are professors, too. So in terms of day-to-day life, it just doesn't matter much.

I think everyone wonders about what might have been. But you can really only make one choice at a time, and so even if you had chosen differently you will still wonder what might have been.

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.

More generally, though, I think there are two main reasons to put algorithms like Gauss-Jordan in the engineering curriculum.

1. While it would be nice to treat linear algebra solvers as a perfect black box, in practice this does not work. Engineers have to be aware of numerical stability issues, how to diagnose when this is an issue, and how to reformulate their routines in a way that resolves the problem. And to do this, they need to know the library of techniques.

A reasonable way of teaching this is to teach Gauss-Jordan, then showing how it goes badly awry, and then showing how things like pivoting can fix it.

2. Personally, though, I find the topic of numerical stability to be a little bit depressing, since it focuses on all the ways computers don't work!

To take a more positive view, a huge fraction of the algorithms in an undergraduate CS course -- from finite automata to parsing to relational algebra to graph traversals -- can be understood as basically doing linear algebra using modules over different semirings (rather than just the reals). Eg, for all-pairs shortest paths, the Floyd-Warshall algorithm is doing an LU decomposition, and Kleene's algorithm is doing Gauss-Jordan.

Not every student will enjoy this, but for the ones who are algebraically minded, it's really exciting to be able to offer them a unified perspective. And then you can show them the GraphBLAS library!

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 Strange Gods:

The population should be homogeneous; where two or more cultures exist in the same place they are likely either to be fiercely self-conscious or both to become adulterate. What is still more important is unity of religious background, and reasons of race and religion combine to make any large number of free-thinking Jews undesirable.

After Strange Gods is a compilation of lectures given at the University of Virginia in 1933. This was the Jim Crow-era Deep South -- and Eliot regarded the outcome of the US Civil War as a disaster.

His grandfather, William Greenleaf Eliot, was a Unitarian minister and abolitionist. One of T.S. Eliot's literary preoccupuations was the degeneration of society. If you contrast his grandfather's life of civic virtue with his cosplay reactionary Anglophilia, you get a pretty good illustration of the principle that every complaint of the conservative is fundamentally just projection.

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 cache, and on ARM (and x86, too, but I'm not sure) these caches are not coherent. So if you modify your instruction stream with a write, you have to clear the instruction cache to ensure that your modified instructions are actually executed by the processor. If you do this a lot, this will make things S-L-O-W, because it forces you to go all the way to main memory to find the next instruction to execute.

This means that if you do want to generate code at runtime, you want to batch the modifications into large groups, so that you have to invalidate the i-cache less frequently. This actually is useful -- it's what JIT compilation is! The reason that JIT can be helpful (even in statically typed languages like Java or Haskell) is that programs often get passed functions as arguments (eg, qsort in C). A static compiler can't optimise these functions much, because you have to know what the function argument will be to do much. But at runtime, you do know what the function is, and by inlining it your code can be made much faster.

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 Nash equilibrium, and be Pareto efficient.

2. Since firms are definitionally teams of people, and since you don't get a choice whether the budget balancing or the workers optimise, this means that firms must sacrifice Pareto efficiency.

3. If firms can't always seek out the Pareto frontier, then a competitive market composed of firms will not satisfy the conditions for Walras' theorem to hold, and so competitive markets can't necessarily reach equilibrium.

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.

If you want to reason about the performance of functional programs, or about the behaviour of imperative/concurrent programs, then you need more sophisticated techniques.

But even in this case, specification composition (taken in the sense of the article, to mean the ability to state properties and proofs in a way which aligns with program module boundaries) has become a relatively routine technique in the last 5-10 years.

Basically, there are three main ingredients we seem to want: (1) you need to understand the abstract resources your program manipulates and how different parts of the program transfer ownership of these resources, (2) you need to understand the protocols (i.e., state machines) that your program components are participating, and (3) you need to understand the rely/guarantee invariants that the program components are maintaining.

Historically, verification techniques have had good stories for one or two of ownership/protocols/invariants (eg, TLA+ struggles with handling ownership), but the research community has developed techniques in the last few years that can handle all of them. As a result, there don't seem to be many small programs out of the reach of program verification -- compositional machine-checked proofs lock-free data structures over weak memory are a thing people can do these days. These proofs are by no means easy, but that's because the algorithms are fundamentally intricate rather than because our proof techniques suck.

We don't have any kind of proof that this is a complete inventory of the techniques we need to verify these kinds of programs. But there is the empirical fact that there are fewer and fewer small programs we don't know how to verify, so it's not an unthinkable possibility.

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 case of the approach he advocates.

The nicest explanation of this fact is in Olivier Danvy and Kevin Millikin's paper Refunctionalisation at Work -- as an example of their program transformation technique, they demonstrate how operator precedence turns into shift-reduce. It's really cute.

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 which you can level up to Johnstone's Stone Spaces.

This approach is suitable for a background logic which is constructive, but accepts the powerset axiom. If you want to restrict yourself to not just be constructive, but also predicative, then the thing to look at is Sambin's formal topology, which he surveys in his 2001 paper Some Points in Formal Topology. (https://www.math.unipd.it/~sambin/txt/SP.pdf)

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 asymptotically the fastest known general CFG parsing algorithm, and is implemented in terms of Boolean matrix multiplication.

The intuition is that bottom-up parsing is basically a transitive closure computation, which is basically the same as solving systems of linear equations over a Boolean ring, which can be sped up using Strassen's algorithm.

A bit of Googling suggests that people have looked at optimising Boolean matrix multiplication on GPUs, but I have no idea what the state of the art here 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, and then write TLA+ formulas to describe the evolution of the system state as the system reacts to events and evolves through time.

In contrast, Petri nets are not a logic. They are a generalisation of finite state machines tuned for describing concurrent processes. In Petri nets, the state is decomposed into a set of "places", and you mark the places with "tokens" to indicate what the current state of the system is. Depending on the state, different state transitions are enabled or not. The variant of state machines that Petri nets correspond to are called "vector addition systems with states" -- basically finite state machines plus a finite number of integer-valued registers. (However, the post this article links to describes a restriction of Petri nets where the markings are 0-1, which makes them exactly the same as FSMs.)

Since the logic of TLA+ describes infinite-state systems, if you want, you can represent Petri nets pretty directly as a set of integer-valued variables and then just write TLA+ formulas about them.

However, the main interest in Petri nets comes from the two facts that (a) they do a good job of describing concurrent systems (you can mix state- and event-based descriptions easily), and (b) are very well-behaved algebraically -- there is a wide variety of constructions which build bigger Petri nets out of smaller ones, which preserve various good properties of the smaller ones. (This latter thing is in fact what the linked post is doing.)

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 right.

See "Donald Trump and vaccination: The effect of political identity, conspiracist ideation and presidential tweets on vaccine hesitancy" in the Journal of Experimental Social Psychology.

https://www.sciencedirect.com/science/article/abs/pii/S00221...

Willie Wong wrote a nice blog post about this a while ago:

https://williewong.wordpress.com/2010/03/18/compactness-part...

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 propositional logic, its resolution proofs are exponentially large. Since modern SAT solvers are basically very fancy propositional resolution provers, this gives you a nice way to find hard instances for them. It also makes the question of when propositional proof systems can be more succinct than one another is also a fundamental question in complexity theory.

2. It also arises in geometry: a compactness for metric spaces is essentially the statement that the pigeonhole principle applies to the space.

I don't have a unified perspective of these two facts, but either one of them is really striking. As a result I'm okay with giving the pigeonhole principle its own natural language name.

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 spaces.

1. The linear tensor product A ⊗ B gets interpreted as the tensor product of vector spaces.

2. The linear function space A ⊸ B gets interpreted as the vector space of linear functions between A and B.

3. The Cartesian product A × B gets interpreted as the direct product of vector spaces (i.e., the categorical product).

4. The sum type A + B gets interpreted as the direct sum of vector spaces (i.e., the categorical coproduct).

5. The exponential !A gets interpreted by the Fock space construction.

This explains why the choice of name is sensible, but I don't actually know if that was the reason why Jean-Yves Girard named it so. If memory serves, he invented linear logic after thinking about Berry's notion of stable functions, but I don't know for sure when the vector space model was invented. (It's not in his 1987 paper, but it can't have appeared very long after that.)

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 means you can prove things about lists-with-positions and basically automatically transport them to statements about gap buffers.

The specification in this note is not an ideal top-level spec, though: it just says there are a series of editor commands that can change one string into another. This is just a basic sanity check, but you can't do much more than that here because the editor state is too impoverished -- it's just the current string.

However, there is an interesting line of attack in (1) enriching the state enough to easily model richer things like command history and undo (eg, by making the state be the whole history of documents and commands), (2) giving each update command a semantics in terms of simple whole-state changes on the enriched state, and then (3) showing that a more efficient representation correctly implements the simple whole-state semantics.

About five years ago, Conor McBride taught a course on dependently-typed programming in Agda in which one of the projects was implementing provably correct text editors, using zippers/gap buffers and interaction via Mealy machines. The link is: https://github.com/pigworker/CS410-15

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 of philosophy into two traditions which largely don't talk to each other represented a great failure of philosophers to live up to the ideals of their subject. It's hard to claim you are seeking wisdom when you are unwilling to listen to your brethren.

Dummett wrote a whole book about this, _Origins of Analytical Philosophy_. It will take substantially more time to read than this article, but on the other hand, it will actually leave you better-informed at the end of it. (He has a hilariously specific answer to when analytic philosophy diverged from continental philosophy: page 62 of Frege's book _The Foundations of Arithmetic_. And it's a really good answer, too!)