solomonb

> But dependent types (and static types in general) don't exist at runtime!

That isn't entirely true when it comes to dependent types and can be seen as a design choice. Types can depend on values and those values can often exist at runtime. Erasure only applies to parts we can determine are not computationally relevant.

For example `Vec n a`. The `n` is a natural number you may need at runtime, such as to get the length without walking the list. A dependent pair `Sigma(n : Nat). Vec n a` carries that `n` at runtime as ordinary data.

In fact many dependently typed languages have techniques, such as quantitative type theory, to assert what is needed at runtime.

We didn't know what investigations were going to lead to RSA or Diffie-Hellman and any particular breakthrough is standing on a mountain of prior work that didn't have an obvious application but nonetheless was necessary to get to a breakthrough.

Honestly I can't believe I even need to state this. Its literally how science works..

> We should evaluate research by the research itself

Why is this the argument when someone challenges your source, but when it comes to someone else's source your argument is:

> This is research from a labor advocacy group, with the explicit aim of the organization to advocate for this sort of thing. This doesn't mean the research is is automatically invalid, but it is bias worth mentioning.

Its pretty clear that there are significant limitations on who has access to the compute needed to drive LLM based scientific research.

what is a 'lo-fi site'?

Given the explosion of interest in proof checkers recently I thought it would be good to promote PLFA. This is an online book that walks you through the basics of logic, programming language design, and formalization using Agda.

I think many people here might be surprised by what writing proofs in Lean/Agda/Rocq/Idris is actually like.

If you have only seen a giant wall of proof output from an LLM then it probably looks like writing some kind of alien "assembly language for math." This couldn't be further from the truth. These are very high level functional languages with sophisticated developer tooling.

Working with a proof checker does more then help you understand the thing you are proving. It teaches you about abstraction, software design, and type theory. I strongly believe this makes you a better software engineer. Its also surprisingly fun and game like!

I've never used Rocq but from what I understand the core type theory is also a version of CIC and like Lean it has strong support for tactics. Rocq defaults to an axiom free core making it constructive. Classical axioms like propositional extensionality and axiom of choice are things you opt into deliberately.

From what I understand the Lean community leans (haha) classical and uses these axioms throughout mathlib. By staying constructive you guarantee that closed proofs can, in principle, evaluate to a canonical form.

I think a lot of people have never actually tried using a proof checker and are forming hot takes based on their imagined assumptions about how they work.

For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):

    +-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z
    +-associative zero y z = refl
    +-associative (suc x) y z =
      suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩
      suc (x + y + z) ≡⟨⟩
      (suc x + y) + z ∎

We pattern match on the first nat to get `zero` and `suc x`. In the `zero` case we have `0 + (y + z) = (0 + y) + z`. Both sides compute to `y + z` and thus the equation holds by reflexivity.

In the `suc x` case we need to show that `suc x + (y + z) ≡ (suc x + y) + z`.

`suc x + (y + z)` computes to `suc (x + (y + z))` by the definition of `+`.

By recursively calling `+-associative x y z` we get `x + (y + z) ≡ (x + y) + z`. Then we need to prove that by congruence this is true under `suc`. We get this by passing our proof (from the recursive call to +-associative) into `ap suc`. `ap` says that given `a = b` it is true that `f a = f b`.

Finally, `(suc x + y) + z` computes to `suc ((x + y) + z)`, so the last step holds by computation, which is why it’s just `≡⟨⟩`.

Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems.

Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof.

This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs.

I would consider using it on any greenfield personal project where I would ordinarily use Haskell.