thaliaarchi

That's a lot of steps in your bootstrap chain. I think tying it to releases can make it easier, but it's good your process is automated.

Rust has a long chain too, but rustc only uses features itself, that the previous release supports. Releases are every 6 weeks.

Go had been bootstrapping from 1.4 (the last C compiler release), until the release of 1.20 this year, when the bootstrap compiler was bumped to 1.17.13 and will be bumped yearly [0]. That meant go1.4 had to be able to compile new versions, keeping the compiler from using new features in itself for 8 years. Notably, this now allows for generics to be used in the compiler.

[0]: https://github.com/golang/go/issues/54265

You should definitely publish that and comment a link! That would be very useful, since you got much further than me.

I like that term. I've tried a couple of bootstrap pilgrimages.

For a job, we needed Go on FreeBSD 8, which entailed a local patch to revert pipe2 to pipe in Go, and building from source. That was my first bootstrap. Go, as Russ mentions, is easy to bootstrap, and I've done it a couple of other times.

I've tried to bootstrap Rust, from its old compiler written in OCaml, but that one is trickier. It has not been maintained like Go's bootstrap compiler and the bootstrap chain has long since been broken. Furthermore, rustc is only guaranteed to be able to be buildable with the previous release. As far as I can tell, no one has built rustboot in many years. I like doing software archaeology, so I'll probably try again with that project sometime.

mrustc takes another approach, closer to the aforementioned GNU Mes, in that it's a reimplementation of Rust, intended for bootstrapping rustc. https://github.com/thepowersgang/mrustc

The malloc design, that led to that yacc bug being discovered, seems to have another interesting property which I didn't see discussed there:

By placing large allocations (those larger than half the page size) at the end of a page, I would think it also allows them to be resized in more cases. Smaller allocations can be then made in the gap, until it's filled. Then, if realloc is called on the large allocation and enough space remains for the difference, it can be shifted backward with memmove. Whereas, the large allocation is placed at the first available position and further allocations are made after it, it has no space to resize.

Disclaimer: I haven't implemented a memory allocator, so my understanding may be off.

I'm surprised to see that the author's ipnsort is not published on crates.io, even though it performs at first or second place on most of the benchmarks for unstable sorts and it passes all the safety and correctness criteria, all while also being able to deterministically panic to inform the user of a logic bug in their comparison function.

https://github.com/Voultapher/sort-research-rs/tree/main/ipn...

I know of at least four MIRs. I used NIR as the name of the IR of one of my compilers. It's not a big deal. Just add qualifiers to your searches.

For source code, I prefer the Software Heritage archive over the Internet Archive, because it archives the git history, instead of the HTML UI. This particular repo was saved there[0] and was most recently visited 24 Oct 2022, which has two more terms updates.

I have created a mirror of this more up-to-date version at https://github.com/thaliaarchi/unity-termsofservice.

Here's how to “cook”[1] an archive from the vault, if you want to do it yourself:

    curl -X POST https://archive.softwareheritage.org/api/1/vault/git-bare/swh:1:rev:28fdae008c61d98d0d9ec55b8cc016ce61809f58/
    wget https://archive.softwareheritage.org/api/1/vault/git-bare/swh:1:rev:28fdae008c61d98d0d9ec55b8cc016ce61809f58/raw/ --content-disposition
    tar xf swh_1_rev_28fdae008c61d98d0d9ec55b8cc016ce61809f58.git.tar 
    git clone swh:1:rev:28fdae008c61d98d0d9ec55b8cc016ce61809f58.git TermsOfService

[0]: https://archive.softwareheritage.org/browse/origin/directory...

[1]: https://archive.softwareheritage.org/api/1/vault/git-bare/do...

Right, not all of the techniques shown yield code that’s correct by construction. For example, an argument was indirectly given, and that error was only found after writing a theorem involving it and finding it was impossible to prove.

In the section “Correct BST by Construction”, they explain the technique of requiring every constructor of a BST to supply a proof that it maintains the properties of a BST. Any modification to a BST constructs a new BST (since Coq is pure), so any operations on a BST must also supply a proof of their correctness. That is correct by construction.

The only useful ltac I see in there is compare, which can save a lot of tedious rewrites, when needing that frequently.

The post also links to some examples of using Wasm to solve complex typographical problems, which I found interesting.

https://github.com/harfbuzz/harfbuzz-wasm-examples

This reminds me of when I used zeroeth, oneth, twoth, and threeth, instead of first, second, and third, for referring to indices 0, 1, 2, and 3 as a TA. It's less verbose than “at index zero”, but feels a little clumsy.

I’m surprised by the low counts for Patient Skeleton. I would have thought stale PRs would be merged more frequently.

For anyone confused here, the “simple” here comes from the simply-typed lambda calculus, that it models. This post addresses several issues with a tutorial paper on a dependently-typed lambda calculus, which is what all the build-up is for.

I would have found this blog post helpful when I was implementing the original tutorial paper, because I got stuck with the higher-order abstract syntax for lambdas. The original uses lambda literals from Haskell, which I couldn't figure it out how to express in Coq or Rust, because of the type recursion and some other issues. Whereas, I would easily be able to implement the first-order alternative presented here in either language.

Additionally, LLVM has MIR (Machine IR), which is what Zig's also stands for. There's a lot of M-starting compiler intermediate representations. This Ruby MIR is Medium Internal Representation. Rust's is Mid-level IR. Similarly, there's MLIR, which is usually expanded to Multi-Level Intermediate Representation.

MIR for Ruby is in no way related to Canonical Mir.

The trick for preserving array lengths in function signatures looks quite useful (e.g., `void foo(int p[static 1]);` for a non-null pointer p). Unfortunately, I think the overloaded use of `const` and `static` somewhat obfuscates its semantics.

Somewhat related to this, printf alone in a loop is Turing-complete, by using %-directives like that. It was introduced in “Control-Flow Bending: On the Effectiveness of Control-Flow Integrity” (Carlini, et al. 2015) and the authors have implemented Brainfuck and an obfuscated tic-tac-toe with it.

[0]: https://nebelwelt.net/publications/files/15SEC.pdf

[1]: https://github.com/HexHive/printbf

[2]: https://github.com/carlini/printf-tac-toe

Andrew Kelley even referenced this in the proposal:

> In exchange, Zig gains these benefits:

> - All our bugs are belong to us.

> - …

The commit that caused OP's bug changed two lines.

https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/lin...

You may also want to take a look at “Deletion: The curse of the red-black tree” (Germane and Might 2014), which presents functional deletion for red-black trees.

https://matt.might.net/papers/germane2014deletion.pdf

How does Datalog with e-graphs compare to Datalog with BDDs in terms of what analyses can be performed? bddbddb is a Datalog engine using BDDs, that, according to their 2005 paper[0], can solve problems like context-sensitive pointer analysis for large programs and analyses implemented with it are faster than hand-tuned implementations in dramatically fewer lines of code. I'm not knowledgeable on what modern Datalog engines are based on.

0: https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf

Do you have a favorite dictionary for Fremdwörter?

From Nand to Tetris: Building a Computer from First Principles

https://www.nand2tetris.org/

How does egglog compare to bddbddb, a Datalog engine powered by BDDs?

They use BDDs in Datalog to solve previously unsolved problems like context-sensitive pointer analysis for large programs and show that analyses implemented with it are faster than hand-tuned implementations and use dramatically fewer lines of code.

https://people.csail.mit.edu/mcarbin/papers/aplas05.pdf

This is the automatic resolution of some instance satisfying a typeclass constraint, and is not related to the termination of functions. This does not call a function. If you compare it to the relational definition I give at the end of the semantics section, the typechecker does not similarly infer satisfying constructers for the relation. Proof tactics can also diverge, but that's different.

I was referring to how the communities of these languages typically frame the problem, so you need formal background to read the materials published on it. As you say, this is a major barrier. This is where Rust shines, in that they've framed the language in terms of how its used, developed accessible documentation, and steered away from delving into the theory behind it.

I was not familiar with loader.c, so I did some digging[0]. It implements the Calculus of Constructions, which Coq is based upon, and generates all programs encoded lower than some value. The search is halting, though very long.

From the analysis[1] in the contest:

> {loader.c}, diagonalizes over the Huet-Coquand `calculus of constructions'. This is a highly polymorphic lambda calculus such that every well-formed term in the calculus is strongly normalizing; or, to put it another way, a relatively powerful programming language which has the property that every well-formed program in the language terminates. The program's main function is called D. … D works approximately as follows: given an argument x, it iterates over all bit strings with binary value less than or equal to x, and, if such a bit string codes for a well-formed program (`term' in lambda-calculus language), it runs the program (`strongly normalizes the term' in lambda-calculus language.) The return value of D is then obtained by packaging together the return values of all these programs. The program's return value is D@@5(99).

[0]: https://googology.fandom.com/wiki/Loader%27s_number

[1]: http://djm.cc/bignum-results.txt

Haskell is notoriously difficult to reason about runtime performance, but that is due to its lazy evaluation, not because it is functional. Lazy evaluation can cause hidden space leaks, where expressions have not yet been evaluated, so maintain references to other values. Most functional programming languages are not lazy.

I think there are varying levels of assurance that developers need while writing software. I tend towards stricter languages with more guarantees, like Rust with its borrow checker and Coq with its powerful types and proofs. This doesn't need to be a universal preference, though; my preferred work is in compilers, which requires a high degree of assurance, and I study programming languages formally.

The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started. I think that Rust has done an excellent job at making stronger systems more accessible, but it takes a lot of conscious work.

With JavaScript, I think the idea that performance in language design can be an afterthought, made up for by world-class optimizing JIT compilers, is fundamentally wrong. It doesn't give users a meaningful way to easily reason about the performance of the programs they write. The main implementation of Python, pythonc, is essentially an interpreter over an unoptimized bytecode format, giving it poor performance. I think performance considerations should be a fundamental part of the language design.