> Basically: I need a Car Object with these exact fields vs give me a thing with the field "foobar" that contains something that I can concatenate with another things.
Um, that's another matter entirely. Polymorphism. Mainstream statically typed programming languages until recently knew exactly one type of polymorphism based on objects, classes and interfaces. It is object-level polymorphism that lies at hear of OOP.
This form of polymorphism is easy to implement in compiler or interpreter, but it also is very limited in expressiveness. So proper functional languages use parametric object-level and function-level polymorphism and allow dictionary passing (both implicit and explicit). This approach filters into mainstream programming language: generics in Java, templates in C++ and so on.
As for resource safety, Haskell is yet to follow Rust and introduce linear types, but many cases are covered by bracket pattern https://wiki.haskell.org/Bracket_pattern which can be enforced on type level using some tricks with ST monad. BTW, it is very similar to RAI discipline suggested by many C++ guidelines, but here it can be enforced.
Again, have fun arguing with objective reality.
>This is true for all formal methods, but here, too, most of them beat deductive proofs.
Sure, feel free to feel superior about that. The problem is, again, type system can be embedded into programming language and allow for quite a bit of guarantees even without full blown dependent types. Java has static typing for a reason.
Sure, to enforce some properties using type system we need an uncomfortably deep delve into type theory or use awkwardly polymorphic code. However, a lot of properties can be enforced with relatively low cost, and Haskell is a long-running research project on what properties are practical to enforce this way.
So, why I need to use proof assistants for properties that can be enforced via practical type system? I really don't see a reason.
>Almost all formal verification in industry uses model checkers and sound static analysis.
But does it happen because it is the only option or the best option? Also, encoding semantics specs is hard, so proper verification of algorithmic side is usually not an option anyway.
>I don't understand why you think it's inferior.
Because it absolutely is. It forces me to use an additional tool when I don't really need to with good enough type system.
Ugh. Look, example: memory safety. For quite some time memory leak needed to be tested for. We have a set of tools for that. Than memory control discipline in C++ arise. And then we have linear types in Rust. With Rust we don't need a separate checker: everything needed to ensure memory safety is embedded into the language type system.
Similarly, with linear algebra basic constrains can be expressed in current GHC type system. However, promoting input values to type level is awkward at best, so Haskell needs a small advancement here. Again, I don't need separate model checker here, moderately advance GHC type system works just fine.
> Of course FOL allows quantification over predicates
Wiki disagrees with you. Oh, well.
>If you are, however, interested in theory (as I am), you can read my series on TLA+.
As I said, at best I might be interested in HOL Isabelle. And even that is doubtful, so far Agda and Coq appear more useful for what I'm interested in.
>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.
>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.
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".
> 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.
>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.
1. Problems with type inference is a problem introduced with polymorphism with implicit type variables and isn't exclusive to dependent types, 'f = show . read' shouldn't compile because of type ambiguity. What is so specific about dependent types in this regard?
>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.
Um, that's another matter entirely. Polymorphism. Mainstream statically typed programming languages until recently knew exactly one type of polymorphism based on objects, classes and interfaces. It is object-level polymorphism that lies at hear of OOP.
This form of polymorphism is easy to implement in compiler or interpreter, but it also is very limited in expressiveness. So proper functional languages use parametric object-level and function-level polymorphism and allow dictionary passing (both implicit and explicit). This approach filters into mainstream programming language: generics in Java, templates in C++ and so on.