3 ms·

>But automation could verify this. Yes, that's what I was arguing. >Except that lots of business logic errors, resource handling errors, and mathematical erro

>But automation could verify this. Yes, that's what I was arguing. >Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false. My experience with formal proofs is it imposes a high cost. I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead (and possibly other costs too). If they exist, they are simply wrong. >I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests. I'm not saying that it does. I'm saying that the kinds of bugs unveiled by formal methods are, in most applications, rare and obscure and the bugs unveiled by integration tests are, in most applications, common and important. When I have limited resources (everybody has limited resources), I tend to take the approach that has the best ROI in finding bugs. For most applications, that isn't formal proofs. >Cool, except that the module integrating these, if validated, would have caught this. You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. >The irony here: BDD is a less formal but similar technique to writing proofs. I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. BDD is simply a means of communicating example driven specs that may or may not be turned into executable user stories. Automated tests (a common side effect of BDD) are not really similar to proofs either. >What is the difference between checking if a program properly closes a socket or if a sorting algorithm works? The likelihood of bugs in the definition are significantly higher the less abstract your code gets. To wit: maybe your presumption that the socket needs to be closed is wrong. >Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules? I absolutely do, that's why I use the right tool for the job.

KirinDave 9y ago
> My experience with formal proofs is it imposes a high cost. What is that experience within the last 5 years. Does it include Idris, Agda, and Coq? > I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead The idea is that by asking humans to make small proofs, the remainder of the majority of additional cognitive overhead can be assumed by the machine. This conversation has a curious pre-assumption that this cognitive load is "new". In fact, it's not. It's an alternative approach to working with the complexity already apparent in our domain. > You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. Why is Peter's comment relevant here? > I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. It is if you care about the results. A lot of modern BDD process has humans as verifiers. And no one's saying that has to go away. But we might need it LESS for certain parts of the system. Certainly in my user-facing fintech applications I have wished for tools that could do this. Sadly a lot of my work in that field predates the usability of a lot of these tools. > I absolutely do, that's why I use the right tool for the job. And the right tool for the job is evidently not a computer? What I think you're missing is that these formal proof systems come with an implicit power: the ability to extend the a more generic type system at build time to reason about your domain. This application is as radical in nature as it is classical. Everyone in every domain has suggested for half a century that we work to bring our code closer to our domain and further from the minutiae of machine implementation. Modern systems seek to do this by creating stable abstractions to build upon. This takes 2 shapes: trained by data (classifiers, regressions, and statistical methods) or refined by logic (proofs, dependent types, type inference and verification). The line between these types is somewhat transient, and over time it's almost certain it will blur. Already we see F# using "Type Providers" that let you use samples derived directly from an API (or specs, or both). These can be obtained as part of the build process, and then the program can be checked against the spec. There is only one real downside to this approach: it makes development require even more computational power. But given that we're solving a much harder problem than the users of our software, the asymmetry seems reasonable. I think you and I agree in the general strokes but you don't like the word "proof", if I'm being honest. I don't know why that word bothers you so much. Did you watch the video? Have you tried Agda, Coq and Idris?

KirinDave 9y ago

> My experience with formal proofs is it imposes a high cost. What is that experience within the last 5 years. Does it include Idris, Agda, and Coq? > I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead The idea is that by asking humans to make small proofs, the remainder of the majority of additional cognitive overhead can be assumed by the machine. This conversation has a curious pre-assumption that this cognitive load is "new". In fact, it's not. It's an alternative approach to working with the complexity already apparent in our domain. > You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. Why is Peter's comment relevant here? > I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. It is if you care about the results. A lot of modern BDD process has humans as verifiers. And no one's saying that has to go away. But we might need it LESS for certain parts of the system. Certainly in my user-facing fintech applications I have wished for tools that could do this. Sadly a lot of my work in that field predates the usability of a lot of these tools. > I absolutely do, that's why I use the right tool for the job. And the right tool for the job is evidently not a computer? What I think you're missing is that these formal proof systems come with an implicit power: the ability to extend the a more generic type system at build time to reason about your domain. This application is as radical in nature as it is classical. Everyone in every domain has suggested for half a century that we work to bring our code closer to our domain and further from the minutiae of machine implementation. Modern systems seek to do this by creating stable abstractions to build upon. This takes 2 shapes: trained by data (classifiers, regressions, and statistical methods) or refined by logic (proofs, dependent types, type inference and verification). The line between these types is somewhat transient, and over time it's almost certain it will blur. Already we see F# using "Type Providers" that let you use samples derived directly from an API (or specs, or both). These can be obtained as part of the build process, and then the program can be checked against the spec. There is only one real downside to this approach: it makes development require even more computational power. But given that we're solving a much harder problem than the users of our software, the asymmetry seems reasonable. I think you and I agree in the general strokes but you don't like the word "proof", if I'm being honest. I don't know why that word bothers you so much. Did you watch the video? Have you tried Agda, Coq and Idris?