Re:Coming Soon: Machine-Checked Proofs in Everyday Development
by KirinDave on Sunday December 31, 2017 @01:02PM
(#16041700)
> 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?
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?