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.
Low-level pointers make everything very very annoying, though.
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.
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 [2] https://github.com/shawa/formal-verification-project
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.
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.
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.
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).
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/
> 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?
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/
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.
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.
That was the impractical part. Exhaustive search scales so poorly it can't be seriously considered.
> 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.
I would agree that heapsort (using an array/list for the heap) would be much harder to prove, but I would expect quicksort to be fairly similar (probably a bit harder).
> 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.
Yeah, I never planned to push research forward with the idea. Primarily, I would like to explore it just to improve my own knowledge; its much easier to know why something is hard once you've failed at it yourself. And perhaps make an interesting toy language.