> 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.
The point is, Polymorphism in dynamic languages is pretty trivial.
There is a reason the golang devs resisted introducing generics for so long, it introduces complexity and can be hard to debug.
If you read my side-note:
> The problem is that types in dynamic languages can easily get super complex without feeling complex while for static languages you might need very advanced features (dependent types and other scary stuff) to represent some cases
If you want to have a functional example: Elm and it's lack of type classes or similar features. There is a reason Elm is resisting to implement a better way to add ad hoc polymorphism for better or worse. It is difficult to fit into the goal of Elm being a simple and easy to use language.
So yes, you can either have a more complex static type system and pay the price for that or just bite the bullet and over specify types.(The problem is also one of ergonomics. Programmer might over specify types because that is the path of least resistance or because things like generics make code harder to debug.)
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.
> 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.
>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.
> 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).
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.
> 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.
> 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.
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".
> 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.
>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.
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.
>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.
> 99% don't need formal verification, they are OK with unit tests.
Formal verification can be cheaper than tests. It's not just about a higher confidence, but also about achieving similar confidence more cheaply. That's one of the reasons why deductive proofs are not so popular in formal methods research -- they're too inflexible.
> If one is actually that concerned with an effort to perform actual verification, they most likely want an actual proof.
But we don't need to hypothesize -- they don't. Almost all formal verification in industry uses model checkers and sound static analysis. If you are interested in addressing the needs of certain small niches, that's one thing, but the thrust of formal methods research is about helping as much software as possible, and so deductive proofs are not the focus, because they're well behind other methods.
> So?
So, if you have a model checker, you don't need to write a proof. The model-checker could automatically provide a model-theoretical proof for you, at the press of a button. That's how, say, avionics software is verified. That's how Intel's chips are verified. People can't afford to write proofs for that volume of software. People write proofs only when model checking fails, or to tie together model checking results. It's no one's first choice (unless they're researchers or hobbyists).
> For decades people didn't care for formal verification.
It doesn't seem like you're familiar with the field. There was a huge boost in formal methods in the 70s followed by a research winter when people over promised and underdelivered. Then, about 20 years ago, there was a resurgence with different goals. In general, research now focuses on managing cost vs. benefit, reducing certain kinds of bugs, and finding ways to make verifiation more flexible, as we've so far been unable to make end-to-end verification scale.
> Why would I care for a method clearly inferior for my use cases?
I don't understand why you think it's inferior. It is absolutely not, and it is superior where it matters most. Expressiveness is the same, so specification is the same, but verification is flexible. You can use deductive proofs, or verifiation methods that have shown more promise.
> I'm very interested how one can express it using, say, first order logic that, you know, doesn't allow for quantification over predicates.
What? Of course FOL allows quantification over predicates and functions if they are elements of the domain, as they are in say, set theory (in fact, there is an assumption at the base of modern logic, that any mathematical theory could be expressed in some first-order language). Or, you could use HOL, if you like. But again, the theory is not the problem here. It's the chosen verification tool (and BTW, formal methods practitioners normally prefer to weaken the specification power if it reduces the cost of verification). Your example, in particular, is easily expressed in FO set theory, or many kinds of many-sorted FOL, or in HOL. For example,
∀ K, V . ∀ f ∈ K → V . ...
is a trivial, perfectly normal, first-order logic over sets. In fact, dependent type theories like Lean's strive to be interpretable in set theory. But really, the choice theory is the least important issue with dependent types or software verification in general.
If you are, however, interested in theory (as I am), you can read my series on TLA+. It is a first-order logic that is strictly richer and more expressive than lambda-calculus-based dependent type theories (unless you deeply embed it in them, and describe your computations in monads): https://pron.github.io/tlaplus
>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.
> But does it happen because it is the only option or the best option?
I don't understand the difference. Model-checking scales better than deductive proofs and is far cheaper. If you have less than 5 years to write a 10 KLOC program or your program is larger, then deductive proofs won't work. Does that mean it's better or that it's the only choice?
> Also, encoding semantics specs is hard, so proper verification of algorithmic side is usually not an option anyway.
This is true for all formal methods, but here, too, most of them beat deductive proofs. With deductive proofs you have to annotate every unit (or work much harder). Model-checking (and concolic tests) can handle partial specifications. This is yet another reason why formal methods research is not focusing its efforts on deductive proofs.
> Again, I don't need separate model checker here, moderately advance GHC type system works just fine.
It doesn't, though. Memory safety is a compositional property, as is every kind of property that can be easily checked by deductive proofs (or almost compositional, requiring one or two inferences). Most correctness properties are not compositional. That deductive proofs (of propositions that aren't compositional) don't scale is not some hypothesis of mine. They've been tried for years, and they just don't. The biggest programs ever verified with them are ~10KLOC and they took years of expert work.
> Wiki disagrees with you. Oh, well.
No, it doesn't. But if you think it does, it means you don't yet know what signatures, theories, structures, interpretations and models are -- the very basics of all formal logics -- so explaining that might take a while (in short, if propositions and functions are part of the structure, of course FOL can quantify over them; if it couldn't, it wouldn't have been the lingua franca of mathematics and the crowning achievement of formal logic). You can read my very short introduction to formal logic here: https://pron.github.io/posts/tlaplus_part2#what-is-a-logic . It's relevant to any formal logic you may want to learn at some point, as they're all more similar to one another than differen, but it may be too terse if you don't have any prior background.
> 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. In general, Lean/Coq/HOL are more geared toward research -- inventing new logics, formalizing "high" mathematics -- and TLA+ is more geared toward industry use and verification of software and hardware, and because that's what I need, that's the one I use most. But it really doesn't matter which you learn -- they're all much more similar to one another than different. Their most important differences are in user-friendliness and their tooling. I would recommend Lean over Coq and Agda, though; I think it subsumes both, and its documentation and tutorials are better, so it's easier to learn. I enjoyed TLA+ and Lean more than Coq and HOL, and I haven't tried Agda. But this could be a matter of personal preference. Again, they're all more similar than different.
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.
Dude, I actually work with dependent type proof assistants (Lean), with a HOL proof assistants (Why3), and FOL/ZFC proof assistant (TLA+'s TLAPS), as well as with a model checker for TLA+ (TLC); I've also worked with a model checker for Java in the past. I have read several books on the subject, and have written two (both available online: https://pron.github.io/tlaplus, and https://pron.github.io/computation-logic-algebra). I've also trained engineers in formal methods.
> Have fun arguing with objective reality.
You've read a few blog posts on one aspect of one formal method, and seem to have not even heard of the majority of software correctness research. You certainly don't seem to have practiced formal methods in industry even using one method, let alone more than one. You don't even seem to know what first-order logic is, what higher-order logic is, and I'm sure that if I asked you the difference between HOL and Martin-Löf type theory, or between classical and constructive mathematics you won't even know what I'm talking about; ditto if I asked you what it means for a type theory to have a set-theoretical interpretation (as Lean's, and maybe Agda's -- I don't know -- type theories do). You've read a few blog posts about a small part of one of the most complex, refractory topics in all of computer science and software engineering. You don't know what the objective reality is.
That you can prove some stuff with dependent types has been true for at least 30 years now. That other approaches, of which you seem to know nothing, scale much better in practice to the point that industry rarely uses deductive proof for anything but small, niche problems and uses model checkers all the time to verify some of the software your life depends on is just a fact. If you don't know what the alternatives are, how can you argue with what I'm saying?
> Sure, feel free to feel superior about that.
I don't feel superior. It seems that, unlike you, I actually use deductive proofs for verification, as well as model checkers, because, unlike you, I actually practice formal verification. But, knowing the tools, I know what works and when. I'm not researching one approach or another; I use which one currently works best, and the reality is pretty clear.
> The problem is, again, type system can be embedded into programming language
Contract systems are also embedded into programming languages. You seem to know one thing (know of, seems more accurate) and argue it's the best, when you have no idea what other things are out there.
> and allow for quite a bit of guarantees even without full blown dependent types. Java has static typing for a reason.
Sure, that because static types are awesome! There are some things -- simple, compositional properties -- for which nothing else works better. Type systems beat the alternatives for these simple properties and, at least currently, lose to the alternatives when deeper properties are involved. Correctness is complicated, and different properties require different tools. That is why, when deep properties are involved, I prefer separating the specification method from the verifiation method. Contract systems are embedded into programming languages and work alongside simple types. They then allow you to choose the best verification tool for the job: you can use deductive proofs, like depdendent types do, and other verification methods when those work better (which is the majority of cases). Dependent types tie you down to the verification method that is the most restrictive and least scalable.
> 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.
You don't. The two are equivalent. I.e., they are equally the least scalable verification method we know. But contract systems, unlike depdent types, allow you to choose: you can use deductive proofs or other, cheaper, more scalable approaches. You need them because deductive proofs -- the only verification approach that dependent types give you -- just don't scale. But I don't need to convince you. I encourage you to learn Idris/HOL/Lean/TLA+/Coq -- whichever one you like (better yet, learn more than one) -- and try writing deductive proofs for large programs. Try different kinds of programs, too: sequential, interactive, concurrent and distributed. Knock yourself out. Perhaps when you speak from experience you'll have a better grasp of what objective reality is. In the process, you will learn a lot, so I truly wish you the best of luck!
But take one piece of advice: don't become dogmatic about something until you've actually looked around. If you argue that X is better than Y and Z because X is all you know, you just sound like a cultist. Learn first, argue later.
I've tried all the methods discussed, and my point-of-view is based on my personal experience and years of involvement with formal methods. You've tried none, and your point-of-view is based on... a couple of blog posts you've read?
Wow. Did not anticipate such a long reply thread. Man it looks like I really should write up a comparison of my (amateur) experiences with TLA+ (TLC + TLAPS), Dafny, Idris, and Liquid Haskell.
Also permeakra, regardless of whether you agree with the points that pron is making here, if you ever find yourself interested in TLA+, I would highly recommend his four part TLA+ series (potentially as an intermediate step after e.g. Lamport's video course). It's absolutely fabulous.
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.