[permeakra]

>More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them.

They are. Anyone working with linear algebra can tell that. Hell, arrays tracking bonds in types rather than in some runtime checks would be a huge thing.

[pron]

> They are. Anyone working with linear algebra can tell that. Hell, arrays tracking bonds in types rather than in some runtime checks would be a huge thing.

That they can be used in a useful way doesn't mean you should have them. Other things (like contract systems) can do pretty much what dependent types do, but don't suffer from as many disadvantages. A tank could get your kids to school, but that doesn't mean it's a good idea to get a tank if what you need is to get your kids to school.

[permeakra]

>That they can be used in a useful way doesn't mean you should have them.

It's a good enough reason to want them as an option.

>Other things (like contract systems) can do pretty much what dependent types do

If you want a system at least as strong as dependent types, you need a system equivalent to dependent types or more generic. Than you can just as well drop the awkward system pretending to not be a type theory and use an actually working formalism.

As far as I can see, Hoare logic is a variant of propositional logic, meaning it is suitable for monomorphic code with static dispatch, but not much more. Extending it to handle more and more generic and more and more polymorphic code eventually transforms it into a variant of type theory (Hoare Type Theory). Might as well start from the side of pure type theory and extend it with linear types - the result should be equivalent.

[pron]

> It's a good enough reason to want them as an option.

I'm not so sure. If you have a good specification mechanism that offers a choice of verification method, why do you need dependent types in addition?

> If you want a system at least as strong as dependent types, you need a system equivalent to dependent types or more generic.

There are many factors by which to judge the utility of specification and verification tools. There is no specific metric of "strength" that determines the value of a formalism. As Alonzo Church wrote in the paper in which he invented the lambda calculus, formal systems are not more or less true or more or less good; rather, they can be more or less convenient for different uses, and more or less aesthetically appealing to different people.

In general, developers need a system that can be flexible. The difference in cost between verifying something with 99.9% confidence and with 100% confidence can be 10x. Sometimes you're willing to pay that 10x for a slight increase in confidence, and sometimes you're not. Often, the decision is different for different parts and different properties of a program, or for different properties of the same part of the program, or for the same property in different parts of the program.

> Than you can just as well drop the awkward system pretending to not be a type theory and use an actually working formalism.

You've studied all logics and all type systems and have concluded that all the type theories are always less awkward to all people than all "direct" program logics?

Also, no logic is pretending to be or not to be a type theory. Type theories are not the canonical representation of logic. That's just not how formal systems work.

> Hoare logic is a variant of propositional logic, meaning it is suitable for monomorphic code with static dispatch, but not much more. Extending it to handle more and more generic and more and more polymorphic code eventually transforms it into a variant of type theory (Hoare Type Theory).

Hoare logic can be used for polymorphism, dynamic dispatch, higher-order subroutine, and anything else type theory can be used for. But I'm not claiming it's superior to type theory. Type theory is fine.

> Might as well start from the side of pure type theory and extend it with linear types - the result should be equivalent.

No, because the problem with dependent types is not the theory, which is, indeed, equivalent to whatever logic you choose and vice versa. The problem is that they force you to use deductive proofs for verification. Not only do you not want your specification method to force you to use a particular verification method, but rather you want flexibility because verification methods vary tremendously in cost, deductive proofs make for the worst default verification methods, as it's the most costly and least scalable (at least so far).

[danielscrubs]

Maybe a sidetrack, but I do think CS majors will find it extremely useful to use deductive proofs when creating libraries.

Think of the implications of when you are checking for sorting libraries you have one that includes a proof that it’s working and maybe even a proof of runtime cost. As a developer you don’t need to write proofs at all as you will not deem it worthwhile. My guess is that this whole popularity contest when checking for a library will lessen considerably (how many stars does this repo have? When was it last updated?)

I’m excited for the future both as a computer scientist and developer.

[permeakra]

> If you have a good specification mechanism that offers a choice of verification method, why do you need dependent types in addition?

Because I don't see it as a good enough method.

> There is no specific metric of "strength" that determines the value of a formalism.

There is, even though it is hard to judge: the number of cases it works for with same amount of work invested and genericity of obtained results.

>Hoare logic can be used

Consider a sorted arrays Arr with elements of type A and integer index ranging from k to l. To express that it is sorted one needs a way to say that \forall n : Int, m : Int, k <= n < l, k <= m < l, n <= m --> Arr(n) <= Arr (m)

Consider an implementation of a relational merge-join operation. To express constraints on the input arrays one needs to express that they have a key to join over and are sorted using compatible comparator over that key, i.e. to introduce predicates referencing predicates in the code.

To me it looks like you have type theory except it moved from typing of variables to associated predicates. I really don't see how it is better.

>The problem is that they force you to use deductive proofs for verification.

I really don't see a problem with it. Granted, I work with academic/numerics software, not enterprise software, and there might be a difference in priorities... But from my side I don't see a problem.

[pron]

> Because I don't see it as a good enough method.

You don't see what as a good-enough method?

> There is, even though it is hard to judge: the number of cases it works for with same amount of work invested and genericity of obtained results.

Well, even deductive proof proponents (like Xavier Leroy) are forced to admit that of all known and practiced formal methods, deductive proofs score lowest of all on that metric.

> To me it looks like you have type theory except it moved from typing of variables to associated predicates.

Then it's not a type theory. A type theory is one way of expressing logical propositions, and, say, first-order logic over set theory is another. You can express similar things in both. Why do you think that it means that one is really the other? If you could say in French the same thing as you can in English, does that mean French is really English?

> I really don't see how it is better.

It's not better! The problem with dependent types is not the theory, which is perfectly fine! The problem is the practice. You can describe a property using dependent types or, say, FOL in some contract system. But only with dependent types you have to verify that property using deductive proofs, the "weakest" formal method by your metric. With a contract system, you can choose to verify the same proposition with a deductive proof, or you can use one of the "stronger" methods.

[permeakra]

I'm sorry, but how you can consider anything but deductive proof as a proof? Inductive 'proofs' are not strict proofs, they are suggestions that need to be tested. Well, except mathematical induction which is said to be a variant of deductive reasoning and can be perfectly modeled with dependent types.

this

> you can choose to verify the same proposition with a deductive proof, or you can use one of the "stronger" methods.

is nothing more than a way to say "you can choose to proof or to do some handwaving instead".