Given proof-assistant builders’ renewed interest in foundational issues, revisiting Hermann Weyl’s classic text [1] is a worthy endeavor. Unfortunately, this paper greatly disappoints.

First, the rather cursory introduction might mislead unwary readers into thinking that the paper is comprehensive. For example, it is strange that the authors don’t mention The seventeen provers of the world [2] in their list of proof assistants. Also, the references are generally incomplete.

An appealing part of Adams and Luo’s framework is the separation between data types and propositions. However, once separated, in order for them to be useful, they have to be linked to each other--this link is never made clear. The authors document some anomalies in their system, which is to be commended, but they do not adequately justify why they made such design choices.

Perhaps the biggest divergence is that Weyl’s system is fundamentally based on relations, while the work in this paper is fundamentally functional. This is a nontrivial difference that casts doubt on the whole enterprise. While much of the paper describes logic-enriched type theory (LTT), the description of what the authors have actually formalized from Weyl’s book is rather short, even though it is supposed to be the main topic of the paper.

Despite the paper’s flaws, it seems as though the authors have done some rather interesting work. Unfortunately, their description of this work leaves much to be desired.