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

[pron]

> I'm sorry, but how you can consider anything but deductive proof as a proof?

Because if the logic is sound and something is true in the model, it cannot be disproven in the logic (and arguably engineers care more about the model, anyway). In other words, you can rely on model-theoretic proofs, which are not deductive (at least not in the logic itself).

Also, I don't think that engineers are necessarily interested in proof, but rather in verification, i.e. knowing that the proposition is true with some probability. This is also more easily achieved in the model theory.

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

No, it isn't. You can choose to model-check (a model-theoretic proof), or you can verify with high but less than absolute certainty. Neither of these is "some handwaiving", and both, BTW, are bigger topics of research in the formal methods community than deductive proofs (take a look at formal methods conferences). And don't forget that because engineers are interested in the correctness of a system, not of an algorithm, there is always a probability that the system would fail, because there is always a probability that the hardware would fail. So below a certain probability, proving algorithm correctness is of no interest to engineers.

It also seems to me that you believe that the ability to write proofs is a choice. This is something that only people who have not used formal methods could believe. In practice, we could not write deductive proofs even if we really wanted to, because it is just too laborious. The largest software ever verified end-to-end using deductive proofs was 1/5 the size of jQuery, and it took world-experts in verification over 10 person-years (it took them 20-30, but they say they can cut it down), and it required an extreme simplification of the algorithms used. So the reality is that we have no idea how to verify programs that aren't tiny using deductive proofs, and that's why most of formal methods research is looking in other directions.

If verifying programs with deductive proofs were an actually viable option, I would be very much in favor. I'm not because it isn't, but there are other verification methods that have so far shown more promise in practice. It's not a matter of principle, but of practical feasibility.

[permeakra]

>Also, I don't think that engineers are necessarily interested in proof,

Depends on the area the engineer works in. Starting from some cost of failure you actually want a proper proof, because the inherent chance of error in incomplete induction becomes unacceptable.

>Because if the logic is sound and something is true in the model,

You can perfectly formalize this model using dependent types and use it there, don't you?

> So the reality is that we have no idea how to verify programs that aren't tiny

Yeah, I know, our brains are to small to properly verify everything, and we need to find ways to outsource as much as possible to machines.

Doesn't mean we need to willfully embrace blind faith in incomplete induction.

[pron]

> Depends on the area the engineer works in.

Sure, but let's say that it's a conservative estimate that 99% don't need proofs. I acknowledged in the beginning that deductive proofs have a place in some niches.

> You can perfectly formalize this model using dependent types and use it there, don't you?

The logic is already a formalization of the model. Yet finding a counterexample in the model directly is very often easier than finding a deductive proof in the logic. Some people got a Turing award for that discovery.

> Doesn't mean we need to willfully embrace blind faith in incomplete induction.

Formal methods is not "blind faith". Second, we haven't willfully given up on deductive proofs; it's just that for decades we've tried to scale them and couldn't, so out of necessity we found methods that have worked better in practice. I don't know if 200 years from now people won't be able to make deductive proofs feasible, but why not use formal methods to make our software better and cheaper now?

In any event, all I want is for people to know (what formal methods research and practice already does) that software correctness is an extremely complex topic, with severe challenges that are both theoretical and practical, and anyone who suggests that there is a known specific solution to the problem or that one of the many imperfect avenues we're exploring is "the future", doesn't know what they're talking about.

[permeakra]

>Sure, but let's say that it's a conservative estimate that 99% don't need proofs

99% don't need formal verification, they are OK with unit tests. If one is actually that concerned with an effort to perform actual verification, they most likely want an actual proof.

>The logic is already a formalization of the model.

So?

>it's just that for decades we've tried to scale them and couldn't,

For decades people didn't care for formal verification. Absolute majority of 'engineers' don't see any use in it. You, on the other hand, see little use for formal verification with dependent types. Well, forgive me for drawing a parallel here.

I want some specific guarantees that are fairly easy to express and keep track with dependent types, not some fancy offshot of Hoare logic. Why would I care for a method clearly inferior for my use cases?

==

Let's return a bit and examine one specific case again. Consider situation: one writes a generic merge-join function over sorted arrays. There, input arrays must sorted with same predicate over same, possibly virtual, key.

To express this in specification on the input data one need to

- quantify over the types of both arrays

- quantify over the type of the key

- and all the functions able to produce a key of this type from elements of array 1

- and all the functions able to produce a key of this type from elements of array 2

- quantify over the ordering predicate over values of the key type

- express that ordering holds for each pair of elements of the array -- i.e. quantify over indicies of arrays 1 and 2.

- For which one needs information on index bonds attached to arrays

I can, with some effort, express it in the language of type theory. I'm very interested how one can express it using, say, first order logic that, you know, doesn't allow for quantification over predicates.