2 ms·

LEAN is another popular language in this area. There are huge benefits for moving the industry in this direction. Such programs that are formally correct elimi

LEAN is another popular language in this area. There are huge benefits for moving the industry in this direction. Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95%. A program can use dependent typing to prove itself 100% correct vs. 100 unit tests which proves only 100 arbitrary test cases as correct. Unit tests are statistical experiments where the people hope that the verification of 100 arbitrary test cases correlates with the entire program being correct. Yes, proofs are harder to write than tests, yes there can be bugs in your proof (their can be bugs in tests too). However, I genuinely believe that for the lifetime of an application, in general, the net benefits of dependent types is positive and greater than that provided by testing. However I do not believe the industry will move in this direction. The reason why the industry won't move in this direction is largely cultural and intellectual. It is harder to learn how to use dependently typed languages and harder to learn how to write a proof of correctness than it is to learn how to write 30 unit tests. Additionally you just need to look at how the industry changes to see that the industry does not trend towards "better" technologies for abstraction. HTML, css, javascript, JAVA, SQL are all awkward/imperfect technologies that dominate the industry for reasons other than technical prowess. Culture dictates their dominance as will it dictate the language of the future. You even get technology that culturally moved backwards simply because people just don't get the importance of static typing... python, php and javascript all came out after typed languages were popular and are all used for large applications where typing would otherwise be very important. Trends like this, and lack of awareness of even algebraic data types tells me that dependent typing is even more unlikely to become popular.

tsimionescu 7y ago
> Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95% I think this is an absurdly high number. The difficulty of proving the kind of rich properties that integration and system-level testing can easily cover is mind-boggling, and also requires huge amounts of infrastructure that doesn't exist and is not feasible for a single team to build. Think of an end-to-end test for a traffic generator application - you simulate a click in a web UI, you start a TCPdump on a network interface, wait for a a few minutes, and sample the capture for some expected packets. How much dependently-typed infrastructure would you need to get even the small level of assurance that this test gives? How much of networking protocols and OS APIs would you have to formally specify to even start proving that your program adheres to them? How much of the DOM and JS APIs would you have to formally specify in order to prove that the button is going to be visible on the screen and that clicking it will produce the right HTTPS calls to the backend? I am reasonably sure that dependent types will continue to get better and will help with developing certain kinds of abstract software components. But I believe that it would take decades before they can become a tool that could be used to prove a realistic large scale program to the point that you can throw away 95% of the testing done today.
- crimsonalucard 7y ago
  Nah I'm going by the testing pyramid. Basically by 95% I mean all unit tests, which under the testing pyramid is the majority. If you follow different philosophies (which is valid and perfectly ok imo) and have more integration tests then unit tests then the 95% marker does not apply. Integration tests or end to end tests or any test that touches IO or tests that measure performance are outside the purview of proofs. Proofs only verify pure logic. Having a full formal model of an end to end system that can be verified with proofs is, I completely agree, really far away. If 95% of your tests are unit tests then my statements apply.

tsimionescu 7y ago

> Such programs that are formally correct eliminates the need for testing almost completely and can cut such infrastructure down by possibly 95% I think this is an absurdly high number. The difficulty of proving the kind of rich properties that integration and system-level testing can easily cover is mind-boggling, and also requires huge amounts of infrastructure that doesn't exist and is not feasible for a single team to build. Think of an end-to-end test for a traffic generator application - you simulate a click in a web UI, you start a TCPdump on a network interface, wait for a a few minutes, and sample the capture for some expected packets. How much dependently-typed infrastructure would you need to get even the small level of assurance that this test gives? How much of networking protocols and OS APIs would you have to formally specify to even start proving that your program adheres to them? How much of the DOM and JS APIs would you have to formally specify in order to prove that the button is going to be visible on the screen and that clicking it will produce the right HTTPS calls to the backend? I am reasonably sure that dependent types will continue to get better and will help with developing certain kinds of abstract software components. But I believe that it would take decades before they can become a tool that could be used to prove a realistic large scale program to the point that you can throw away 95% of the testing done today.

crimsonalucard 7y ago
Nah I'm going by the testing pyramid. Basically by 95% I mean all unit tests, which under the testing pyramid is the majority. If you follow different philosophies (which is valid and perfectly ok imo) and have more integration tests then unit tests then the 95% marker does not apply. Integration tests or end to end tests or any test that touches IO or tests that measure performance are outside the purview of proofs. Proofs only verify pure logic. Having a full formal model of an end to end system that can be verified with proofs is, I completely agree, really far away. If 95% of your tests are unit tests then my statements apply.