Re:Coming Soon: Machine-Checked Proofs in Everyday Development
by KirinDave on Sunday December 31, 2017 @01:07PM
(#16041741)
> Here's my hypothesis: The problem with these static verifiers is that they are applied at the wrong stage.
They can be applied at lots of stages. Why not apply them to all of them?
> Either your program (or code unit) is sucessfully verified or it isn't.
This is demonstrably false. It can help you write better, safer code incrementally. Every approach that is discussed here has a "refinement" plan.
> Imagine instead writing code that is made "safe" using run-time asserts everywhere.
I can imagine this, it's the C/C++ style of code circa 2010. It's awful for users. But it's not what we're discussing here.
> If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications?
Yes. You're already seeing two major examples of this: Type Providers and derivations of dependent types fall into one camp, dependent type implementations (of which the most prominent is Idris) fall into the other. All of them offer the ability to extend the type system and make proofs useful to developers even as they also help make code total and enforcible.
I think it's further along than you seem to suggest. Can I suggest you grab a copy of Atom, Atom-Idris, and go through some Idris tutorials? You can also try F# and use Json samples pulled from an API to generate types that inform your tooling and improve code quality.
They can be applied at lots of stages. Why not apply them to all of them?
> Either your program (or code unit) is sucessfully verified or it isn't.
This is demonstrably false. It can help you write better, safer code incrementally. Every approach that is discussed here has a "refinement" plan.
> Imagine instead writing code that is made "safe" using run-time asserts everywhere.
I can imagine this, it's the C/C++ style of code circa 2010. It's awful for users. But it's not what we're discussing here.
> If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications?
Yes. You're already seeing two major examples of this: Type Providers and derivations of dependent types fall into one camp, dependent type implementations (of which the most prominent is Idris) fall into the other. All of them offer the ability to extend the type system and make proofs useful to developers even as they also help make code total and enforcible.
I think it's further along than you seem to suggest. Can I suggest you grab a copy of Atom, Atom-Idris, and go through some Idris tutorials? You can also try F# and use Json samples pulled from an API to generate types that inform your tooling and improve code quality.