Reg, thanks so much for your comment. I'm really happy you appreciate the value.
It's very interesting that you put the focus in the descriptive language. I've been working on that for a long time. It's not finished, but some areas are clarified. Indeed, after reading your comment I think I will try to focus on getting somewhere workable with that part first.
This whole project is so big. It will be good to do it in the open and use as much help as I can.
The paper starts out with a simple sort implementation, and then adds static proofs of correctness for:
A) Totality (Termination/no infinite loops)
B) Length of output = Length of input
C) Output is sorted
It does not prove the one-to-one mapping, and I don't know how hard that would be to prove (intuitively, it does not sound like it should be too hard).
The dependent types approach lets you write a program while reasonably controlling its algorithmic complexity and operational behavior -- and still have its mathematical meaning proven to match a specification.
I think a title like "I want to fix programming" is a bit over the top -- given that it is a hard problem with very smart people working at it. It is more acceptable, in my opinion, to "fix programming" after learning in detail what the state of the art already entails. That means knowing Agda, Coq, Logic languages, Hoare logic, etc.
Thanks Peaker. I know a bit about dependent types, and how complex types sytesm can help a lot. Indeed, the title is a bit over the top (or maybe even too much over the top!). Hopefully the attention will help get some extra hands & brains.
At the very least, all the pointers I'm receiving are really valuable.
I don't claim I can fix it, but I definitely want to fix it, have some ideas, and I'm willing to work, listen and learn!
And if I think I can add something, is that I come from a practical/industrial background. Most of my work has been in C++. I'm looking for practical tools for everyday work.
It's very interesting that you put the focus in the descriptive language. I've been working on that for a long time. It's not finished, but some areas are clarified. Indeed, after reading your comment I think I will try to focus on getting somewhere workable with that part first.
This whole project is so big. It will be good to do it in the open and use as much help as I can.