3 ms·

> Once you've done enough theorem proving, you'll really start to appreciate the core benefit of functional programming and understand why academics abundantly

> Once you've done enough theorem proving, you'll really start to appreciate the core benefit of functional programming and understand why academics abundantly use it over imperative coding I do already appreciate functional languages. And I have struggled to keep myself from adding functional elements to the language. A large part of why functional programming is easy to reason about is that functions are pure. This would be included in the language; by default everything would be pass by value with references needed an environment to be passed as well (to keep them pure). It still reads like an imperative language though.

seanwilson 9y ago
Either way, you're not going to get around that proving general program properties beyond very basic ones is very difficult to automate and very challenging to do manually. Even with decades of work and teams of researchers, we still can't make this easy for pure functional programs yet. Have you tried existing theorem provers?
- thethirdone 9y ago
  > Either way, you're not going to get around that proving general program properties beyond very basic ones is very difficult to automate and very challenging to do manually. What are you considering basic? Would proving that matrices of the form vv^T/(v^Tv) are idempotent (for a fixed ) be basic? That is about the maximum I would be shooting for this language to automatically prove. Additionally, for many assertions it would make sense to be able to fall back to a runtime check if it can't be proved easily. If you want to prove something more advanced writing, out all the steps of the proof as assertions should make it trivial to do the automation. > Have you tried existing theorem provers? I have used Coq. I have actually written a first order logic prover (which only worked with single variable predicates).
  - seanwilson 9y ago
    > What are you considering basic? The problem is it's really difficult to constrain how hard the proof goals are going to be. Even if you're only interested in properties to do with the length of lists/arrays which are about is simple as you can get, you quickly get into undecidable areas (i.e. there cannot exist an algorithm that can always generate the proof or tell you it's unprovable) and you have to resort to manual proofs. More advanced properties like if a data structure is sorted are even more unpredictable. Look up verifying sorting algorithms in theorem provers like Coq and Isabelle which have been around for decades; you'd assume basic properties like these would be easily automated by now but that's not the case. > Additionally, for many assertions it would make sense to be able to fall back to a runtime check if it can't be proved easily. There's a few system like this already e.g. https://sage.soe.ucsc.edu/ https://sage.soe.ucsc.edu/ > I have used Coq. I have actually written a first order logic prover (which only worked with single variable predicates). Did you find the manual proof challenging when you tried to verify basic algorithms?
    - thethirdone 9y ago
      > Even if you're only interested in properties to do with the length of lists/arrays which are about is simple as you can get, you quickly get into undecidable areas. AFAIK, most of the undecidable areas in current solvers are not truly undecidable but rather practical limits. A full search of all proofs up to some arbitrary depth could solve pretty much any real problems, but would be impractical. I don't know much about avoiding practical undecidability though as the prover I wrote was complete (or at least I believe it is and it seems to be true in practice). > There's a few system like this already e.g. https://sage.soe.ucsc.edu/ https://sage.soe.ucsc.edu/ Thanks for mentioning Sage. I am not familiar with it. > Did you find the manual proof challenging when you tried to verify basic algorithms? I have been using insertion sort to benchmark the hypothetical language with, and I found proving insertion sort to be correct in Coq to be fairly easy. It definitely wasn't trivial, but coming from a background of formal proofs on paper, it was easy.
      - seanwilson 9y ago
        > AFAIK, most of the undecidable areas in current solvers are not truly undecidable but rather practical limits. A full search of all proofs up to some arbitrary depth could solve pretty much any real problems, but would be impractical I wouldn't agree with this. Look up inductive proof automation which you need when working with user defined data structures and properties like in your examples. It's still very hard to fully automate these and researchers have been trying at this problem for decades. The branching factor in the proof search is essentially infinite so you cannot just do an exhaustive search. Have a read about inductive proof automation in ACL2 and Isabelle for example to see what is currently possible. > I have been using insertion sort to benchmark the hypothetical language with, and I found proving insertion sort to be correct in Coq to be fairly easy. It definitely wasn't trivial, but coming from a background of formal proofs on paper, it was easy. That proof will be fairly easy because the algorithm, data structure and the program property definitions will all have a similar shape which won't be the case for e.g. quicksort or heapsort. Keep going with your idea, I just mean to be aware that you're hitting against problems that are well known to be very difficult, have lots of existing related work and are still current research areas. Coq etc. are a long way from being mainstream because of this.

seanwilson 9y ago

Either way, you're not going to get around that proving general program properties beyond very basic ones is very difficult to automate and very challenging to do manually. Even with decades of work and teams of researchers, we still can't make this easy for pure functional programs yet. Have you tried existing theorem provers?

thethirdone 9y ago
> Either way, you're not going to get around that proving general program properties beyond very basic ones is very difficult to automate and very challenging to do manually. What are you considering basic? Would proving that matrices of the form vv^T/(v^Tv) are idempotent (for a fixed ) be basic? That is about the maximum I would be shooting for this language to automatically prove. Additionally, for many assertions it would make sense to be able to fall back to a runtime check if it can't be proved easily. If you want to prove something more advanced writing, out all the steps of the proof as assertions should make it trivial to do the automation. > Have you tried existing theorem provers? I have used Coq. I have actually written a first order logic prover (which only worked with single variable predicates).
- seanwilson 9y ago
  > What are you considering basic? The problem is it's really difficult to constrain how hard the proof goals are going to be. Even if you're only interested in properties to do with the length of lists/arrays which are about is simple as you can get, you quickly get into undecidable areas (i.e. there cannot exist an algorithm that can always generate the proof or tell you it's unprovable) and you have to resort to manual proofs. More advanced properties like if a data structure is sorted are even more unpredictable. Look up verifying sorting algorithms in theorem provers like Coq and Isabelle which have been around for decades; you'd assume basic properties like these would be easily automated by now but that's not the case. > Additionally, for many assertions it would make sense to be able to fall back to a runtime check if it can't be proved easily. There's a few system like this already e.g. https://sage.soe.ucsc.edu/ https://sage.soe.ucsc.edu/ > I have used Coq. I have actually written a first order logic prover (which only worked with single variable predicates). Did you find the manual proof challenging when you tried to verify basic algorithms?
  - thethirdone 9y ago
    > Even if you're only interested in properties to do with the length of lists/arrays which are about is simple as you can get, you quickly get into undecidable areas. AFAIK, most of the undecidable areas in current solvers are not truly undecidable but rather practical limits. A full search of all proofs up to some arbitrary depth could solve pretty much any real problems, but would be impractical. I don't know much about avoiding practical undecidability though as the prover I wrote was complete (or at least I believe it is and it seems to be true in practice). > There's a few system like this already e.g. https://sage.soe.ucsc.edu/ https://sage.soe.ucsc.edu/ Thanks for mentioning Sage. I am not familiar with it. > Did you find the manual proof challenging when you tried to verify basic algorithms? I have been using insertion sort to benchmark the hypothetical language with, and I found proving insertion sort to be correct in Coq to be fairly easy. It definitely wasn't trivial, but coming from a background of formal proofs on paper, it was easy.
    - seanwilson 9y ago
      > AFAIK, most of the undecidable areas in current solvers are not truly undecidable but rather practical limits. A full search of all proofs up to some arbitrary depth could solve pretty much any real problems, but would be impractical I wouldn't agree with this. Look up inductive proof automation which you need when working with user defined data structures and properties like in your examples. It's still very hard to fully automate these and researchers have been trying at this problem for decades. The branching factor in the proof search is essentially infinite so you cannot just do an exhaustive search. Have a read about inductive proof automation in ACL2 and Isabelle for example to see what is currently possible. > I have been using insertion sort to benchmark the hypothetical language with, and I found proving insertion sort to be correct in Coq to be fairly easy. It definitely wasn't trivial, but coming from a background of formal proofs on paper, it was easy. That proof will be fairly easy because the algorithm, data structure and the program property definitions will all have a similar shape which won't be the case for e.g. quicksort or heapsort. Keep going with your idea, I just mean to be aware that you're hitting against problems that are well known to be very difficult, have lots of existing related work and are still current research areas. Coq etc. are a long way from being mainstream because of this.