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..

This is such a short sighted take. Number theory was considered beautifully useless for centuries, and now it’s the backbone of the cryptography that secures every bank transaction. We don't know where the pursuit of knowledge will take us.

Thinking in such a utilitarian way feels like a flavor of Meditations on Moloch.[1] Just look at how short-term, quarter-to-quarter thinking is affecting the economy and the lived experience of every human on earth. It’s horrible.

[1] https://slatestarcodex.com/2014/07/30/meditations-on-moloch/

> 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.

I think Spaceship Earth goes a bit further back: https://en.wikipedia.org/wiki/Spaceship_Earth

what is a 'lo-fi site'?

I made a project for this earlier this year: https://github.com/solomon-b/friendly-ghost/

You can can read from Loki or Journald and use regex or alert levels to filter what you pass to the LLM.

I've been using it with deepseek for my homelab. Its pretty helpful.

What a wonderful response :)

> I'm going to be thinking about that for a while.

This is a deep and fascinating world to get into. Enjoy!

> It led me to a kind of branching, graph-like manner of learning...

Yes! I love this experience. It takes a little owrk but you can even import the 1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.

The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.

If you wanted a place to get started I would highly recommend PLFA: https://plfa.github.io/

> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression

I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.

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.

The secret of Lean4 is that its actually a great programming language, sort like a super Haskell. In fact I like it more as a programming language then as a proof checker!

Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.

"sufficiently capable" is doing an insane amount of heavy lifting here. Like you can only interpret a theory into another one if the target is at least as strong as the source and even then "to and from" is a MUCH stronger condition that most pairs of theories do not satisfy.

Then when a translation exists the proofs can blow up in size to where you lose feasibility and understandability even tho they are technically still proofs.

Regardless of all that, I wasn't even bringing up 1lab because of the choice of language or type theory. I bring it up as an example of a pro-human way of presenting formalization.

Yup, Mikan is a fork of Agda that focuses specifically on Cubical Type Theory. Lean's CIC is only one approach to dependent type based formal verification. Cubical gives you a computational approach to Homotopy Type Theory.

The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free."

All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.

If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev

Thanks! My goal is to turn it into an interactive website like https://1lab.dev but a book would be cool too.

And if you want to see worked examples elaboration of dependent types then the `elaboration-zoo` is a great thing to look at:

https://github.com/AndrasKovacs/elaboration-zoo

I've also got an incomplete project that aims to present a more expanded set of implementations then the elaboration zoo: https://github.com/solomon-b/lambda-calculus-hs

Ed Kmett is one of the smartest people I have ever met in my life. He is quite literally built different.

He completed undergrad and graduate programs in math, computer science, and a special program in ai all simultaneously in 3 years. I believe he was finishing programs before his scholarships could kick in.

The natural numbers are countably infinite. For each n ∈ ℕ, there is a proof by reflexivity that n = n. Hence there are countably infinitely many such proofs, one for each natural number.

Continuing to develop my LPFM radio station www.kpbj.fm

- We have accumulated almost all the equipment needed to setup our FM broadcast. The main piece of equipment we still need is the EAS Decoder.

- Our studio space build is in progress. I recently welded some tables for the booth and found an old Orban Optimod for our airchain.

- We have over 80 shows and our roster continues to grow.

If you are in Los Angeles or love community radio please reach out.

Did you have previous experience with formal verification and/or dependent types?

But CNC machining still requires a ton of physical skills. Its true that you maybe aren't planning out and executing every single tool pass by hand but there is still a tremendous amount of knowledge and physical skill that goes into setting up, indicating parts, etc.

okay maybe i was wrong about them being technically endangered, i misread that somewhere. Still doesn't change the fact that we shouldn't be abusing animals to have pseudo-intellectual psychedelic experiences.

Can we please leave the fucking toads alone?

This is an endangered species getting massively abused by the wellness "shaman" industry. It fucking sucks. Just use synthetic 5me0-dmt if you really must do a goofy vision quest larp.

I am responding to a comment that is framing the reduced size as a good thing from an obesity perspective...

Is obesity more or less prevalent now versus 1991?

The churn in this space puts javascript to shame. As an example, its only been a few months and AFAICT no one is even talking about openclaw anymore.