4 ms·

I have been playing around with an idea for a programming language that enables practical theorem proving. The core idea behind it is that statically proven as

I have been playing around with an idea for a programming language that enables practical theorem proving. The core idea behind it is that statically proven assertions would be really powerful. Loop invariants can be simply expressed as an assertion inside the loop. Additionally, to give it a bit more power; assertions could be given the ability to act over sets (say over all ints). This might look something like XY = {int, int} @assert commutative fn add(a XY, b XY) XY { return (a[0]+b[0], a[1] + b[1]) } fn commutative<a,b>(f (a,a)b){ assert x,y: f(x,y) == f(y,x) } And then it would also be helpful to add on assertions to types so assignments to variables also checks the assertions order = enum {greater, equal, lesser} comparator<a> = (a,a)order fn sorted<a>(pair ([]a,comparator<a>))bool { (l, cmp) = pair if l.length() <= 1 { return true } return cmp(l[0],l[1]) != order.greater & sorted((l[1:],cmp)) } SortedList<a> = ([]a,(a,a)order) & sorted There are a few major issues with my idea currently (it really requires dependent types to be ergonomic and allocation and pointers could be strange) which have prevented me from making a quick demo compiler or language spec. But I would be very excited to discuss it.

PeCaN 9y ago
Reminds me a lot of LiquidHaskell, you should take a look at what they've done if you haven't seen it yet. It's a very good idea IMO. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
ghkbrew 9y ago
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
VladimirGolovin 9y ago
Have you looked at F* ? It's a Microsoft research language based on a subset of OCaml augmented with Z3 theorem prover: https://www.fstar-lang.org https://www.fstar-lang.org Here's how the assertion of commutativity would look in F*: val f : int -> int -> Tot int let f a b = a + b let commutative = assert (forall a b. f a b = f b a )

PeCaN 9y ago

Reminds me a lot of LiquidHaskell, you should take a look at what they've done if you haven't seen it yet. It's a very good idea IMO. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/

ghkbrew 9y ago

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

VladimirGolovin 9y ago

Have you looked at F* ? It's a Microsoft research language based on a subset of OCaml augmented with Z3 theorem prover: https://www.fstar-lang.org https://www.fstar-lang.org Here's how the assertion of commutativity would look in F*: val f : int -> int -> Tot int let f a b = a + b let commutative = assert (forall a b. f a b = f b a )