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?
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.