7 ms·

Have you looked into research regarding refinement types? Because they describe almost exactly what your reaching for (types with assciated provable assertions)

Have you looked into research regarding refinement types? Because they describe almost exactly what your reaching for (types with assciated provable assertions). Specifically Liquid Haskell[0] extends Haskell with (dependent) refinement types, but keeps the type checking decidable and the proof burden relatively light by using a restricted predicate language and an SMT solver. [0] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/

thethirdone 9y ago
Yeah, I am aware of refinement types. You can do a lot of what I am envisioning with just refinement types. Expressing loop invariants with just refinement types is really awkward though. The main reason why the language I am envisioning is not a functional language is because Idris, Liquid haskell, ... have already explored many of the related ideas. I want to take ideas from them and bring it into an imperative language as that hasn't been as well explored.
- tom_mellior 9y ago
  You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com/ http://frama-c.com/), or SPARK Ada (https://www.adacore.com/download https://www.adacore.com/download). There has been quite a lot of work in imperative languages that might inspire you. Low-level pointers make everything very very annoying, though.
  - thethirdone 9y ago
    > You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com/ http://frama-c.com/), or SPARK Ada (https://www.adacore.com/download https://www.adacore.com/download). I am aware of SPARK. KeY and Frama-C are new to me though. Thanks for mentioning them. > Low-level pointers make everything very very annoying, though. Definitely.
- shawa_a_a 9y ago
  To throw another one onto the _have you looked at X_ pile, Microsoft Research has put a lot of effort into the Why3 theorem proving platform, which is the backend for the verifier built into their (experimental?) verifier-aware, imperative language, Dafny[1]. It feels very much like writing C#/Java but with verified pre/post conditions, loop invariants etc. I took a formal verification course in college that involved writing several verified sorting, search etc. algorithms in Dafny [2]. I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. (At the time I didn't realise that not only does the checker check the program, but compiles it into a CLR-compatible binary, hence you'll see equivalent C code for comparison) [1] https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny [2] https://github.com/shawa/formal-verification-project https://github.com/shawa/formal-verification-project
  - c-cube 9y ago
    Just to give credit where it's due, I believe why3 is developed purely by LRI, a public french research lab (see http://why3.lri.fr/ http://why3.lri.fr/). It's indeed used as a proof backend in several tools, including frama-C and Dafny (Microsoft Research), but otherwise it's from academia.
  - thethirdone 9y ago
    > To throw another one onto the _have you looked at X_ pile, I am pretty sure I have seen Dafny before, but it wasn't on the top of my head. Thanks for mentioning it. > I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. I agree with both of those statements. I am not thinking of something revolutionary. I have been thinking of a few ways to make it more ergonomic than Dafny though. Refinement types would be one of the key ways to do that. I think all of the key capabilities would be the same though. It would probably make sense to make a transpiler to Dafny to try it out.
- seanwilson 9y ago
  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: it makes programs an order of magnitude to reason about for both you (when you have to write manual proofs) and the machine (if you want proof automation). To make it practical to verify imperative programs, you're likely going to end up imitating a functional and stateless style to get anything done anyway.
  - thethirdone 9y ago
    > 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).

thethirdone 9y ago

Yeah, I am aware of refinement types. You can do a lot of what I am envisioning with just refinement types. Expressing loop invariants with just refinement types is really awkward though. The main reason why the language I am envisioning is not a functional language is because Idris, Liquid haskell, ... have already explored many of the related ideas. I want to take ideas from them and bring it into an imperative language as that hasn't been as well explored.

tom_mellior 9y ago
You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com/ http://frama-c.com/), or SPARK Ada (https://www.adacore.com/download https://www.adacore.com/download). There has been quite a lot of work in imperative languages that might inspire you. Low-level pointers make everything very very annoying, though.
- thethirdone 9y ago
  > You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com/ http://frama-c.com/), or SPARK Ada (https://www.adacore.com/download https://www.adacore.com/download). I am aware of SPARK. KeY and Frama-C are new to me though. Thanks for mentioning them. > Low-level pointers make everything very very annoying, though. Definitely.
shawa_a_a 9y ago
To throw another one onto the _have you looked at X_ pile, Microsoft Research has put a lot of effort into the Why3 theorem proving platform, which is the backend for the verifier built into their (experimental?) verifier-aware, imperative language, Dafny[1]. It feels very much like writing C#/Java but with verified pre/post conditions, loop invariants etc. I took a formal verification course in college that involved writing several verified sorting, search etc. algorithms in Dafny [2]. I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. (At the time I didn't realise that not only does the checker check the program, but compiles it into a CLR-compatible binary, hence you'll see equivalent C code for comparison) [1] https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny [2] https://github.com/shawa/formal-verification-project https://github.com/shawa/formal-verification-project
- c-cube 9y ago
  Just to give credit where it's due, I believe why3 is developed purely by LRI, a public french research lab (see http://why3.lri.fr/ http://why3.lri.fr/). It's indeed used as a proof backend in several tools, including frama-C and Dafny (Microsoft Research), but otherwise it's from academia.
- thethirdone 9y ago
  > To throw another one onto the _have you looked at X_ pile, I am pretty sure I have seen Dafny before, but it wasn't on the top of my head. Thanks for mentioning it. > I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. I agree with both of those statements. I am not thinking of something revolutionary. I have been thinking of a few ways to make it more ergonomic than Dafny though. Refinement types would be one of the key ways to do that. I think all of the key capabilities would be the same though. It would probably make sense to make a transpiler to Dafny to try it out.
seanwilson 9y ago
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: it makes programs an order of magnitude to reason about for both you (when you have to write manual proofs) and the machine (if you want proof automation). To make it practical to verify imperative programs, you're likely going to end up imitating a functional and stateless style to get anything done anyway.
- thethirdone 9y ago
  > 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).