[el_pollo_diablo]

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible.

Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs.

Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.

That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change.

That is not to say that dependent types do not have their use. Where they shine is at module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately.

[penteract]

> dependent types and total functions do not scale.

I'm not convinced that this is much more true than the claim "correct code doesn't scale". If you add to your code in a way depends on a new property for correctness, and the code was not previously written with awareness that the new property was necessary, then you need to check through the rest of your code and make sure that the property is maintained. Formally verifying things is painful because it actually makes you check this.

Instead, we live in a world where we use software that is not completely correct. Browsers have remote code execution vulnerabilities because people who make browsers decided it's more important that javascript can run quickly, and that new standards get implemented, than that we avoid such vulnerabilities at all costs.

[less_less]

I agree to some extent with your thesis. But also you don't have to encode all the properties of the program in dependent types everywhere. You can have the implementation contain either no proofs or fairly few (e.g., termination and no UB, which can often be automatically discharged), and then separately prove things about it. E.g.

    def function_spec bleh blah := math_blargh
    def function_impl bleh blah := code_blargh
    theorem function_correct: forall bleh blah, function_impl bleh blah = function_spec bleh blah := by { long proof }

or whatever. That way the function's spec and implementation remain separate and readable. In my limited experience, Lean code usually works more this way rather than having the whole function and its spec in a giant dependently-typed object. For imperative code you can also use Hoare triples and vcgen, but that's currently only partly baked (i.e. proving things is a giant pain).

Maintenance is still a headache. If you change a small piece of your code, you would then need to change all the proofs that refer to it, and then if the specs also changed then you need to change all proofs that refer to those specs, etc.

[el_pollo_diablo]

In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical properties as the value is moved around. That is why I mentioned them in the context of opaque types. This is especially useful with generics: when a type parameter is instantiated with a dependent type, all its occurrences instantly benefit from the strong typing.

They can also be used to enforce just enough constraints on the inputs of a function to make it total, but this comes down to the tradeoff between either leaving an error path in the program and proving its unreachability later, or not having this error path but immediately requiring the proof. In any case, as you mention, further properties can be proved later without altering the dependent type.

I do not intend to come off as overly negative about dependent types. They have their uses, but they can also bring a maintenance nightmare.

[prplfsh]

It's my own ignorance speaking, but is this as true in math? I could see this being a problem for programs where you have few, if any, real axioms and the axioms themselves change. But if we're talking math, the axioms should be fixed.

[smj-edison]

Most math does proofs somewhat informally (as in the proofs are written in a conversational style, and they're considered valid when they convince the majority of mathemeticians), but those proofs can be traced back to ZFC (a specific formulation of set theory and first order logic).

Type theory, especially dependant types, are a pretty recent development, and aren't really used in practice in math. Even in Mathlib (what most people mean when they say they've used lean), they encode first order logic. The proofs are dependently typed, but the actual logic of the proof is all in ZFC.

[gugagore]

> they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it")

I understood you to be saying "bundling is encouraged", in the sense of

https://leanprover-community.github.io/glossary.html#bundled...

I'm not sure it's encouraged. I agree that it felt natural to define a type like NonNegativeInteger, or a wrapper type like `Sorted(T)` to indicate that that wrapped list is sorted. But I think this is an area of style and aesthetic that is still emerging, far from ossified.

The problem of "threading" new things within existing programs is an important one to address, and it has multiple solutions (context management, dynamic scoping (lol), implicit arguments, type classes). I am curious if the claim of "does not scale" is mitigated by one of those solutions...

[yorwba]

> you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.

Having to do this is a sign that the new property depends on implementation details in some way. This can definitely feel like annoying busywork when there is only one reasonable implementation. Of course your sorting algorithm doesn't change the multiplicity of elements in the array, you wouldn't write a bug like that. Of course your sorting algorithm doesn't change the order of elements that are already sorted correctly, you wouldn't write a bug like... except unstable sorting algorithms do that and are widely used for performance reasons. So you do have to check your actual implementation step by step to verify that it really does what you think it must of course be doing. Trying to separate the concerns does not change this.

[el_pollo_diablo]

I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one shouldn't lead you to alter the first proof. But it does if you carelessly use some logical tools like dependent types and single preconditions/postconditions/loop invariants.

For example, take Hoare's while rule (see https://en.wikipedia.org/wiki/Hoare_logic#While_rule). If you have already proved

    {P∧B}S{P}

and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove

    {Q∧B}S{Q}

or even

    {P∧Q∧B}S{Q}

if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove

    {P∧Q∧B}S{P∧Q}

which is incomparable and uselessly mixes both concerns.

[yorwba]

You don't have to edit ("throw away") your original proof, it's just that a single proof covering the most precise description of the program's behavior is more compact than restating the program code a bunch of times plus the additional ceremony to assert that all those proofs refer to the same program.

[el_pollo_diablo]

> a single proof covering the most precise description of the program's behavior is more compact

Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We have compilers with LTO for that, though; we would never maintain source code in that form.

Snark aside, I get your point about restating the program code, but this can be alleviated by interactive proof assistants that largely reduce the length of proof scripts. This is mostly a matter of tooling.

[yorwba]

Yes, if you don't mind the repetition or have tooling to deal with it, you can have multiple separate proofs, dependent types won't stop you.

[armchairhacker]

The key is to structure the program so that only a tiny trusted core is verified but the properties extend to untrusted code. For example, the sel4 microkernel is formally proven to not crash (barring hardware), so any program running on it will not crash the entire computer, just itself. Or (only parts of it are formally verified, but) the Rust borrow checker practically guarantees any Rust code without `unsafe` will not produce memory errors; any amount of lines of Rust code, without any proofs themselves, are covered by the relatively tiny trusted core that is the borrow checker.

[rafaelRiv]

I would say that the value of dependent types in software engineering isn't in proving all code correctness. As a user pointed out in the idris2 Zulip, most programs using dependent types don't have, and shouldn't have, proof of validity for the entire program. Instead, you simply get more correct code by construction, and I think that's the whole point.

I'm currently developing a unikernel in idris2, and the experience is very pleasant (unfortunately, I'm not quite ready to share it yet).