jules

I just tried the editor for Rust and it is great. I love the way errors and warnings are displayed. The navigation mode is also a brilliant idea. For larger files however, the screen real estate used by the navigation on the right hand side is not quite big enough for me. You still have to scroll a lot and hunt for what you want to find.

It would be great to somehow display more things to navigate, possibly using more of the screen (especially if you're using a big external monitor), possibly with some visual of the dependencies between them (so that you're not trying to find things in a long linear list). Especially when you're browsing new code the dependencies would be very helpful to get a quicker understanding of the structure of the code, and for your own code they might also suggest ways to refactor/reorder code in the file.

I'll definitely try out this editor for the next couple of days, and maybe switch from VS code. I find the comments of the people saying that they won't pay for an editor quite strange. I would gladly pay $24.99 per year for a 1% productivity improvement.

Wouldn't it be amusing if a common english word like "foundation", usually referring to the thing on which buildings are constructed, is uniquely reserved for the all the kinds of things on which you can theoretically build all of mathematics, but where none of the people involved are actually trying to do that, and a different word has to be invented for a similar thing, because you got banned out of the club for trying to actually build mathematics on top of it.

ZFC is the x86 assembly language of foundations. Saying that ZFC is good enough because you can do all of mathematics in it is like saying that we don't need Java/Rust/Python because x86 assembly is good enough because x86 assembly is Turing complete. True, but that's missing the point of what people are trying to do with higher level languages.

You can theoretically do everything you want in ZFC, but it's low level and a bit outdated and you don't actually want to write formal proofs in it. We know from experience that it is possible to translate the kinds of proofs that people do on paper into formal ZFC proofs, at least in theory. The mathematicians that study ZFC-like foundations are OK with that "in theory"-qualifier and are instead investigating the theoretical properties of the foundations.

The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics in, and computer proof assistants are being developed that make it possible to actually write down formal proofs in them, in the form of proof code. For this to work it needs to be possible to translate all the kinds of arguments that mathematicians write down on paper into formal proof steps. It is not sufficient to remark that it is theoretically possible to find some kind of translation: it must actually be done for the computer to accept the validity, and the burden must not lie on the mathematician writing down the proof. Instead, the system must make it easy to write down the steps that the mathematician wants to do. One of the kinds of arguments that mathematicians use on paper is that if A is isomorphic to B, then a theorem about A automatically gives you a corresponding theorem about B. Homotopy type theory is trying to formally enable this kind of reasoning.

In summary, the foundations people interested in ZFC have a very different goal than than the foundations people interested in (homotopy) type theory. The fact that the ZFC people are perfectly happy with ZFC and only care about ZFC doesn't mean much. The goals of the type theory people are not achieved by ZFC, not by a long shot.

Note that it is not the case that the general body of mathematicians cares about ZFC and does not care about HoTT. They care neither about HoTT nor about ZFC. The nod to ZFC that mathematicians give when pressed is mere lip service; most mathematicians would not even be able to list the axioms of ZFC. Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.

The coke bottles themselves are amazing too. I used to go to school with a reusable bottle filled with milk. Those cylindrical lunch bottles for kids were absolutely horrible. They leaked half the time, spoiling my bag and notebook. If you dropped them they would break because they were hard plastic. The rubber ring that was supposed to stop it from leaking would degrade quickly and start to smell funny. Those things cost as much as 20 bottles of coke, and an empty coke bottle is a vastly superior product in almost every way!

Great post!

How does this compare mimalloc, the other allocator from Microsoft? https://github.com/microsoft/mimalloc

The number of early cases connected to the market could be partly confirmation bias -- you detect an early case at the market, and then start to investigate everyone connected to the market, and surprise! almost all of the cases you find are connected to the market.

Yes I think that's right :) I think I have a way to visualize what's happening more clearly than the | notation I used above.

We have grammar: S -> 'a' S 'a' / 'a'

I'm going to put (aSa) around parses of the first alternative and <a> for the second alternative. So a successful parse would look like (a(a<a>a)a).

Here's what the PEG parser will do for aaaaa. It will first recurse all the way down, trying the first alternative at every point:

    (a(a(a(a(a
            ^

The choice indicated by ^ will fail because it is expecting another 'a', so that choice will be backtracked, and it will replace the ( with < at that position:

    (a(a(a(a<a>
          ^  

Now it will backtrack over that ^ choice and replace the ( with < at that position:

    (a(a(a<a>a)
      ^

Now comes the key point: the next thing it backtracks over is the second ( and NOT the third (, because the third ( actually succeeded. So it has skipped over one extra layer.

Now it will parse:

    (a<a>a)aa

This one succeeded, and consumed 3 characters. The rest of the input is then still to be parsed by productions further up the stack, but since this S is the main production of the grammar, we declare failure because the whole input was not consumed.

In general, after backtracking, a bunch of ('s may initially seem to succeed, and then when it fails it will backtrack over all those, rather than over just one of them.

For your larger example:

    (a(a(a(a(a(a(a
                ^

    (a(a(a(a(a(a<a>
              ^

    (a(a(a(a(a<a>a)
          ^

    (a(a(a<a>a)a)a)

So this one does parse the whole input.

> Well, now I'm grateful I've never had to implement a parser for anything more complicated than a Lucene-style query syntax.

Interestingly, these problems don't seem to come up in practice. But things like this are still a good argument for LR/GLR parsers: LR parsers will report the conflict at grammar compilation time, and GLR parsers will backtrack with all possible choices, so they will parse the way you'd expect. They are certainly the more principled choice. But in practice it may not matter that much in practice because people don't seem to use these kind of grammars, at least not for programming languages.

The right mental model for PEGs is not whether or not it will parse the entire string. PEGs will attempt to parse some prefix of the string and then stop and leave the cursor there. Here is a list of strings and how far it will parse (hopefully correct):

    a| 
    a|a 
    aaa| 
    a|aaa 
    aaa|aa 
    aaaaa|a 
    aaaaaaa| 
    a|aaaaaaa 
    aaa|aaaaaa 
    aaaaa|aaaaa 
    aaaaaaa|aaaa 
    aaaaaaaaa|aaa 
    aaaaaaaaaaa|aa 
    aaaaaaaaaaaaa|a 
    aaaaaaaaaaaaaaa| 
    a|aaaaaaaaaaaaaaa 
    aaa|aaaaaaaaaaaaaa 
    aaaaa|aaaaaaaaaaaaa 
    aaaaaaa|aaaaaaaaaaaa 
    aaaaaaaaa|aaaaaaaaaaa

Consider your example aaaaa. The PEG will parse the first a, and then the recursive call will parse from a|aaaa. Now the next recursive call will eventually fail. Therefore the first recursive call will only parse one a, and then return back to the initial call which will parse another a. So the final state is aaa|aa.

At a high level, the reason for this behaviour is that PEGs are greedy. The inner recursive calls will always parse as much as they can, without regard for the outer calls that still want to parse more a's.

Yes you're right, I had already edited that while you were posting your reply. I thought you wanted to point out the usual simple "a" / "aa" problem.

I think it will parse "a", it will parse "a a a", and "aaa a aaa", and "aaaaaaa a aaaaaaa" and so on, but nothing else.

PEGs are a compact notation for recursive descent and they compile to recursive descent parsers. What would be the advantage of writing the compiled code by hand?

This is a good point in favour of context free grammar based parser generators. I think the trade-off is a bit more subtle though.

CFG semantics is nice and declarative when we specify which strings belong to the language, but a parser is a function from strings to parse results, and then the nice semantics stops working due to ambiguities. The PEG semantics on the other hand naturally expresses such a function, and the function you get with PEG semantics is almost always the function you want.

When we look at character level grammars, the CFG formalism doesn't work well either. They fundamentally rely on greedy lexical token matching.

Extensions such as indentation sensitive parsing and user defined operators quite naturally fit into PEG style semantics, and are more difficult to integrate into CFGs.

CFG based parser generators are way more complicated internally than PEG based parser generators, which are extremely simple.

Choosing to not consume or disseminate a piece of content is not censorship. Censorship is when you attempt to make that choice for somebody else.

I can't explain it but every time I hear that phrase I get a very visceral feeling of injustice. The phrase represents extrajudicial punishment by a mob or powerful entity, and the negation of fairness, proportionality, and due process, often expressed by a person who does not care because they are certain that they themselves will not fall victim to abuses of such systems.

Why do you think that R would be below 1 with a 100% vaccination rate? In countries with 80-90% vaccination rate we still see massive spread. Handwaving about "nonlinear effects" doesn't cut it. Vaccine mandates are a very heavy tool, that needs very heavy justification.

There is no magical law of physics that ensures that a 100% vaccination rate gets R<1. It all depends on how transmissible Omicron is in vaccinated people. The numbers are currently still in flux, but a reasonable current estimate is that two vaccinations are approximately 70% effective against hospitalisation with Omicron. We also know that it is (much) less effective against transmission than it is against hospitalisation. Even if it were 70% effective against transmission, that might still not be enough to get R<1 given the ease at which Omicron spreads.

Compare, say, with the measles, which has a natural R of about 10. With a 70% effective vaccine, it would still spread. Luckily we have a vaccine that is 99% effective against transmission, so it can be stopped. COVID vaccines are not nearly as good.

To give some indication from my country (the Netherlands) where 86.3% has been fully vaccinated, of the positive corona tests, approximately 66% fully vaccinated. We can see that this 66% is less than 86.3%, indicating that the vaccination is somewhat effective at stopping transmission, but that's still a heck of a lot of vaccinated people who can catch and transmit covid.

> Even if it were true that R would still be > 1 with a 100% vaccination rate, as long as the R rate is lower with the vaccines than it is without the vaccines, the vaccines are preventing (some) transmission.

Of course, but in the long run it would make little difference, because as long as R>1, then more and more people will continue to catch the disease, just over a longer period of time. Smearing out infections can be important if there is a shortage of hospital beds, but this can hardly be called "stopping transmission".

> The more contagious the virus, the higher your vaccination rate needs to be, for reasons that I hope are obvious.

Absolutely correct! And at a certain point, unless the vaccine is 100% effective against transmission, the vaccination rate would need to go above 100%, which is clearly not possible.

Secondly, many lifestyle choices affect the rate of transmission. The singular focus on the forcing people to inject something into their body against their will is unethical (note: I have personally been vaccinated). It is unethical not just because it violates bodily autonomy, but also because it is an easy way to abdicate from your responsibility to take care of your other lifestyle choices that affect the spread.

> We really, really need to starve the virus of hosts, particularly so we don't breed ever more variants.

Not going to happen. Even at a 100% vaccination rate it would still have many human hosts as the data I quote above show, but also because many wild animals now have COVID too. Unless they develop a new vaccine that is much more effective than the ones we currently have, there is no stopping it any more. We need to learn to live with it, like we do live with the flu. We are lucky that Omicron is so much milder than Delta. If you are fully vaccinated then the chances that you have serious illness are very very low. It for sure is terrible for old people and those with existing health problems, but we cannot realistically do anything about that, except for instituting Chinese level control. The response against COVID is at this point completely irrational and doing more damage than COVID itself. Not just economically (which directly translates into future deaths), but also because it is tearing societies apart.

100% vaccination rate would still have R>1. While that is unfortunate, they are right and you are not.

Single threading is not the issue. Just 5% of single modern core should be plenty fast enough to run a text editor. You still want multiple threads of course, to avoid blocking the UI for background work, but computers are so fast nowadays that it should still be fast enough even if all threads were run on the same core.

Food, water, and air regulations are completely different. To be analogous, they would have to be regulations about food and drinks you must consume, or gasses that you must breathe in. Even if that were the case, it would still be less invasive than an injection with RNA, which enters your cells, which causes your cell to produce spike protein, which causes your immune system to attack those cells. Note again: I personally did take the vaccines, the point is that this is not comparable to food regulations. When I did take the vaccine I already knew that medically there was no necessity: due to my age and no comorbidities the risk of complications from COVID was known to be extremely low, and I knew that it wouldn't help other people either because it would not get R<1, but I simply made the decision because I did not want to lose my sense of smell for a couple of months. I was under no illusion that I was saving the world with that decision. If one was under such illusion, I can certainly understand the frustration with other people not saving the world. But this is not reality.

Your point about schools mandating vaccines is good. I'm not categorically against vaccine mandates. For a sufficiently transmissible disease, which is also deadly, and where spread can be stopped by vaccination, it can be justified. Measles may be a candidate: very transmissible (more so than COVID) and deadly for children (2.6 million deaths in 1980), and a vaccine which is extremely effective (99% immunity against infection) and has a long term safety record (complications <1 per million). COVID is not such a disease, and the COVID vaccines are not such vaccines.

Even so, in my country it is not compulsory to get vaccinated against the measles, not even in schools. Certainly one does not have to show a measles vaccination proof when entering a non-essential business like a restaurant, which one does have to show for COVID. Nor does one have to get a booster every 9 months, which one does, by law, for COVID.

> I’m talking out of frustration that I’ve made lifestyle changes to help others who clearly don’t feel the need to reciprocate.

Ok but this is not a good reason to compel other people to vaccinate. These people likely did not ask you to make the changes that you did. Nor are the changes that you made likely to have made much difference in the lives of these people, and whether or not these people do get vaccinated has a very minimal impact on your life, other than your frustration.

The fact that you feel like it would be a nice gesture from them if they "reciprocated" by getting vaccinated does not weigh against the negatives. Many of these people are probably genuinely afraid to take the vaccine. They may be very misinformed, but the fear is real. If you put sufficient pressure on these people via the government, for instance by threatening to take away their job and their ability to provide for their children, then they may well take the vaccine. But these people may resent those who forced them into it for the rest of their lives, and feel alienated from a society that made them do it. And some of them will feel ill for a day or two (as many do after getting the vaccine), which may cause them to think that any future pain or health problems were caused by the vaccine. It this worth it to you in order to act out your frustration that they "don't feel the need to reciprocate"?

The rate only becomes highly relevant if it makes the difference between R>1 and R<1. Otherwise the disease will still exponentially expand, just over a more spread out period of time. Even countries with very high vaccination rates now have R much above 1, so the idea that COVID can be stopped by vaccines is unfortunately not tenable any more.

We have traditionally not violated bodily autonomy for very low probability of benefit to other people, and I think the precedent that some countries have set is a grave mistake. I understand that you are upset and afraid of death, but I would encourage you to look at the statistics. If you are vaccinated then COVID is a very survivable disease. Without vaccination, the average person's risk of dying of COVID is approximately 0.5%. The vaccine trial showed that it is 98% effective, so it cuts your risk by another factor of 50. As a point of comparison, if you are unvaccinated then COVID is ~10x more dangerous than the flu. Vaccination changes that picture. Consider whether your reaction is proportionate, when compared to what your reaction to "people murdering you from across the room with the flu" would have been. Ethical violations have historically happened quite often when people are irrationally afraid. It is true that the vaccines are less effective against Omicron, but on the other hand Omicron is a milder disease than Delta. Current data is looking like we are net very lucky to have Omicron displace Delta.

A vaccinated person can still spread the disease. Perhaps at a lower rate, but a lot of lifestyle choices affect that rate. The singular focus on that one choice is irrational and the obsession with what other people inject into their bodies is unethical, since the free choice of a person to inject or not inject a substance into their body is more fundamental than many of the other choices that affect the rate of spread.

I have personally been vaccinated but I feel a pang of guilt whenever I use the government mandated vaccine passport to make use of restaurants and so on. So I stop using those facilities that require a vaccine passport, with the exception of the gym.

I think this conveys the right intuition but it's a bit finicky and artificial to make that concept precise so I think it's better to say that the concept of moving through spacetime at a given speed is not well-defined.

Particles have a trajectory through spacetime. They don't move along the trajectory because the time dimension is already part of the trajectory. So the speed at which they move along their spacetime trajectory seems to be a meaningless concept.

What is true however is that if the particle takes a clock with it, and you mark a tick every second the clock ticks, then the ticks will be equally spaced along the trajectory (where distance is measured using the Minkowski metric).

This makes a bit more precise what it means for photons to be stationary along the time dimension. It does not mean that they move horizontally in a space-time diagram. They move diagonally at speed c, as you expect, so for an outside observer they do move through time. However, the Minkowski distance between any two points on photon trajectories is zero. So if you wanted to annotate their trajectory with the clock tickmarks you could start somewhere and put your first tick there, but then your second tickmark would be infinitely far away on their trajectory.

Thus, for an outside observer, a clock approaching the trajectory of a photon would appear not to tick.

From a different point of view, we can reason by analogy to Euclidean geometry. When we have a curve through space we can talk about the tangent vector at any point. But the length of the tangent vector is not a well-defined concept. Only its direction is. You can define the length of the tangent vector for a particular parameterisation p(t) but for the curve itself, i.e. the set {p(t) : t in R}, the length of the tangent vector is not defined.

It is similar for a curve through spacetime. We can parameterise a curve with some variable x and write the curve as {p(x) : x in R} but this is just a set and the length of the tangent vector of p(x) depends on which parameterisation you chose for the curve. But the data of how a particle moves through spacetime is only the curve {p(x) : x in R} itself, not the function p(x): different parameterisations describe the same physical situation as long as the set {p(x) : x in R} is the same.

I find it fascinating that you call me nonsensical for making the very reasonable assumption that energy consumption will stay the same for a back-of-the envelope calculation, and here you are talking about infinite improvement factors.

> I didn't say a word about basing something on fossil fuels.

You said: "Yes, but that doesn't imply you need the capacity to run the country 100% on batteries for a week. That's just not something anyone would ever do. For example, a gas turbine with a low duty cycle would definitely be cheaper than a battery after a certain period of time. So why would you use a battery for that?"

> I don't see how we "seem to agree". The comment I initially responded to

Note that I responded to that comment with a calculation showing that that plan is economically infeasible. The scenario is not all all contrived; what that person proposed we need is reasonable, and it would in fact be quite dangerous and insufficient to have only one week's worth. Years in which there is more than a week without wind and hardly any sun (due to winter) occur approximately every 10 years in Germany. Thus calling a week's worth of storage contrived is just wrong. If anything, it's contrived in the direction of not being enough.

The specific factor for cars is not relevant. The factor of 3 is wildly optimistic for general energy use. The point is that even taking the factor of 3, it's still extremely expensive.

Regarding the second paragraph: if you point is that it would be cheaper to duplicate a significant portion of our energy generation, one based on renewables and one based on fossil fuels for safety...that is perhaps true, but that only proves the original point, so I'm a bit confused why you phrase your replies in an antagonistic tone of voice when we seem to agree.

I just googled solar battery cost and took the cheapest in the result that came up: https://www.solarchoice.net.au/blog/battery-storage-price/ It is possible that the numbers that come up there are too high.

A factor of three (which is very optimistic) doesn't change the conclusion: a week's worth of storage is not feasible with current battery technology, let alone a few weeks.

How much storage would actually be required is not clear to me. It depends on a lot of factors. A week doesn't sound totally crazy to me; we certainly want a good safety margin so that society doesn't collapse in a bad winter. If we take super optimistic numbers and have one day of storage and take your factor of 3 reduction in energy use, then the cost of storage alone would still be about twice what we currently pay for the energy. Expensive but certainly a cost that would be possible to pay.

Generating that amount of energy using nuclear would cost approximately $13.4 per person per day (IIRC ~3x what we're currently paying for it). Note that I have not included the cost to generate the energy in the $130 storage costs, but that cost is negligible compared to the $130 anyway.

The environmental damage would probably also be much less with nuclear, versus a ton of solar + wind + batteries. But there would be disaster danger. It is unclear to me how the danger of nuclear disaster would compare to the danger of running out of stored energy in a winter month.

> Storing a weeks worth of consumption on a 'per person' basis can be done for a fraction of $1m.

How?

Since the costs of storage are currently so huge, it seems to me that if you want to go the solar + wind route, it makes sense to overprovision energy generation. That would reduce the amount of storage you need, and the extra energy during summer would be somewhat useful. Note however that you would need massive amounts of wind+solar.

For an average household to satisfy its electricity needs, it needs ~10 average size solar panels (assuming perfect storage). However, household electricity use is only 5% of our energy use. So to satisfy energy needs with solar, you need approximately 200 solar panels per household. Even if you round that down to 50 due to reduction in energy consumption and use of wind energy, it's still a lot. But the Netherlands is obviously not a very good country for solar. In countries like Australia, the numbers would look way better.

Let's approximate the cost of that. The energy consumption of my country (the Netherlands) was 3157 PJ in 2017. This was 980 kwh per person per week. Solar batteries cost a bit more than $1000 per kwh. So at these prices this plan costs approximately $1 million per person. Solar batteries last 5-15 years. If we say that they last 20 years, then the energy storage costs are $130 per person per day per week's worth of storage. This plan sounds feasible if costs come down by factor of 10.

Dependent types go beyond what Zig does by removing the distinction between comptime variables and runtime variables (so types can depend on runtime variables). Zig goes beyond dependent types in the sense that the comptime/runtime distinction allows Zig to handle all comptime values at compile time, which is important for efficiency. It would be interesting to combine the two approaches, via partial evaluation or staging.

I've noticed that reading is faster than listening at 3x speed. A quick way to test this is to enable subtitles.