Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.

Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.

It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?

2.2 beta 1 was released last week. Testers welcome!

Has the bug with removing autoloaded functions been fixed yet?

If you mean the fact that a removed autoloader function may be autoloaded again, then yup, that's fixed in 2.2. Here's the issue that tracked it: https://github.com/fish-shell/fish-shell/issues/213

When is 2.2 planned?

I saw that ;-) The translation is:

  do {

    to.set((from = from.shift(1)).get(-1));

  } while(--count > 0);

which looks correct to me. Hence my question what orodley thinks is wrong.

I think you might be looking at the wrong thing on the Wikipedia page. The core feature of Duff's Device is interleaved switch and do statements:

  n = (count + 7) / 8;
  switch (count % 8) {
  case 0: do { *to = *from++;
  case 7:      *to = *from++;
  case 6:      *to = *from++;
  case 5:      *to = *from++;
  case 4:      *to = *from++;
  case 3:      *to = *from++;
  case 2:      *to = *from++;
  case 1:      *to = *from++;
          } while (--n > 0);
  }

(extraneous register statements removed for conciseness)

That would be a bug in the translation. We'll investigate. Thanks!

Yes indeed. We handled goto into do-while statements wrong. Fixed now. Thanks!