Ask HN: Any logic based software dev tool which helps building code gradually?

Good to know ty!

What are the main differences (pros/cons) using TLA+ vs Dependent Types (and proving the algorithm is fine) for system verification?

I am a high-schooler and I understand dependent types. (I am not the person you are replying to, but I am the person who first mentioned typed holes.)

In type theory, there are things called "terms" and "types." A term is something like `fun x -> x`, or `(1, 2)`, or `1 + 1`. In short, a term is basically an expression. Each term has a type. For example, `fun x -> x` might have the type `a -> a` and `(1, 2)` might have type `Nat * Nat`. If a term has a type, it "inhabits" the type. "x has type T" is written `x : T`.

According to an idea called the Curry-Howard correspondence, types can encode logical statements such that terms that inhabit the type are its proofs. Therefore, by inhabiting a type, you are really proving a theorem.

With dependent types, the term and type languages are the same language, so you can mix them together. In short, types are terms.

Here are some types in Martin-Lof type theory:

    ---------
    () : Unit

The unit type is a type with one inhabitant, (). It can be interpreted as the type of the empty tuple. In the Curry-Howard correspondence, the unit type corresponds with truth.

    x : A    y : B
    --------------
    (x, y) : A * B

A * B, the product type of A and B, is the type of pairs. It is based on the Cartesian product operation: https://en.wikipedia.org/wiki/Cartesian_product In the Curry-Howard correspondence, the product type corresponds with logical conjunction (and). By proving A and proving B, you can prove A * B (AKA A /\ B).

    x : Empty
    ----------------
    elim-empty x : a

The empty type is the type with no inhabitants. If you have an inhabitant of the empty type, you can eliminate it to derive anything. The empty type corresponds with falsity, and its elimination means that false implies anything.

    x : A
    --------------
    Inl x : A + B

    x : B
    --------------
    Inr x : A + B

The sum type is the tagged union, meaning "this or that." The type A + B means that the Inl tag holds an A and the Inr tag holds a B. The sum type corresponds with logical disjunction (or).

    f : A -> B    x : A
    -------------------
    f(x) : B

The exponential type, the type of functions, means logical implication. If you have f, a proof that A implies B, and x, a proof of A, you can prove B by doing f(x).

With dependent types, the product and exponential types are generalized into the dependent sum (sigma) and the dependent product (pi) types respectively.

With the dependent sum type, or sigma type `Σ (x : A) B(x)`, the second component in the type is actually a function of A (meaning that B : A -> Type). The dependent sum type generalizes the product type so that the type of the second element of the pair is actually dependent on the first element. In the Curry-Howard correspondence, the sigma type corresponds with existential quantification, "there exists" or "for some." To prove Σ (x : A) B(x), you must inhabit A (show that A exists) and B(x) (where B is a logical statement about x, the inhabitant of A).

With the dependent product type, or pi type `Π (x : A) B(x)`, B is also a function of A that returns a type. The dependent product type generalizes the exponential type so that the codomain of the function, B(x), is dependent on the function's input, x. The dependent product type corresponds with universal quantification, "for all." To prove Π (x : A) B(x), you must prove B(x) for every possible x, where B(x) is a logical statement about x.

Why the dependent product type generalizes the exponential type and the dependent sum type generalizes the product type seems confusing at first glance, but it really isn't:

Σ for x = 1 to n, B(x) = B(1) + B(2) + ... B(n), a...

I'm 25, have been into dependent types for about a year, and studied maths at uni (specialising broadly in logic and other similarly pure and foundational things).

F# simply because I was looking for a functional-programming job and this was one of the first that came up. (Great personal fit, using technologies I'm not ill-disposed towards, good pay etc.)

Ah, I did not know that!

The Purescript integration seems definitely interesting!

Do you use these tools for work?

Yeah, I actually use `int` for this (because 90% of the time, if I genuinely want to use an int, I've tiny-typed it so that an int won't type-check) - but being able to see the things that are in scope of the right type at the same time would be amazing. I recognise that it would take a somewhat idiosyncratic F# coding style to make this useful, though.

Cool group. I'm already enjoying the podcasts (and kudos for having transcripts available, as well).

Yes sure! I did not mean the tool should exist independently, I meant some kind of extra IDE "layer" beside a "regular"/widespread (C,Java,C#) compiler/language. But ofc there is no such thing like "regular" compiler/language

That group seems really cool! Thanks!

Thanks for pointer!

Yes sure!

I did not mean the tool should exist independently, I meant some kind of extra IDE "layer" beside a "regular"/widespread (C,Java,C#) compiler/language. But ofc there is no such thing like "regular" compiler/language