Nice article, here is the direct link since no one commented on the HN post.

A tale of four theorem provers - https://blueberrywren.dev/blog/primes/

> Broadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small "proof kernel" containing base rules (e.g. forall x, x = x) that all proofs must be constructed via.

In all my years of reading - and I've written my fair share of dangling prepositions - this is the first time seeing "via" at the end of a sentence. Let me guess the author is German, Danish, or a mathematician.

These abbreviations were not defined before use.

- LCF: Logic for Computable Functions - https://en.wikipedia.org/wiki/Logic_for_Computable_Functions

- HOL: Higher Order Logic - https://en.wikipedia.org/wiki/HOL_(proof_assistant)