[gonzaw]

Hello.

Recently I've started studying type theory, and most specifically constructive type theory (CTT) with induction (using Coq).
I have to say.....damn, and I thought learning Haskell was mesmerizing.

I just can't stop thinking about types and dependent types and inductive types and constructing proofs when looking at code. This makes me sad when I have to go back to projects in Java or other languages /> .

On the other hand, I see CTT and I can't help but to think it could be made so much greater. CTT is a lamda calculus, where the only think you have are terms, contexts, and judgements. This can be modeled to a Functional Programming paradigm pretty okay (e.g Coq can be translated to Haskell), but what about other paradigms? Or what about other aspects of programming?

For example, CTT, or lamda calculus, don't have a way to make I/O part of their intrinsic theory. Or how about programs themselves? CTT can't really model a series of instructions as far as I know. Or for example, model threads, and model concurrency.
Imagine being able to use Coq's proof assistant to prove your code is thread-safe and will never result in deadlock or any concurrency baddies?
Imagine being able to model and prove that your background thread is calling a web service appropiately, and does what it specifies?
Imagine being able to create a security system, and prove it can't be hacked, or if it can, know exactly how by proving which scenarios it can happen in?
I would kill to be able to program in that! And like I said, maybe include other paradigms as well, like OO. Include objects, state, behaviour, inheritance, associations, etc into the theory.

I feel like there is such a bigger world to go into! I love learning CTT, but I've searched and I haven't found anything that does the above.
Do you guys know of any new language, theory, research, or something that might tackle issues like that?


Another doubt I have is: Are there any OO languages, or maybe procedural ones, that have an extensive type theory similar to CTTs? I'm thinking dependent types, hierarchy of types, functions as first class citizens, types as first class citizens, etc
I use Java generally, and I can't help but look at generics and sigh in disappointment, knowing all the things I could do if I could use Coq's type theory instead of it.
I've googled but I couldn't really find anything, other than languages similar to Coq (i.e Agda, and Omega or something like that).


Anyways, this may be a little off topic, but it's what my "vision" is:
I imagine a world where a programming language exists, where it can be used for any practical application imaginable, and you can prove it works within the same language (barring some incompleteness it'd carry).
There would be no need for "testing", if you want to test something, you don't create a Unit Test, and hope you didn't miss any case that might brake it, you effortlessly and easily use a proof assistant to prove your code works.
For some subset of programming, specially Functional Programming, this is already done with proof assistants like Agda or Coq. But that subset of programming isn't really practical. I want it to be mainstream, I want it to be used everywhere, I want it to be applied to anything you could want programming applied to.
I'd like to know if there is anything that resembles or tries to resemble that.

Anyways, sorry for rambling so much. I'm basically intending this to be a general discussion of these ideas and subjects, not just a question about a specific problem, error, etc.

Thanks

[Momerath]

gonzaw, on 05 November 2013 - 05:59 PM, said:

Imagine being able to use Coq's proof assistant to prove your code is thread-safe and will never result in deadlock or any concurrency baddies?
Imagine being able to model and prove that your background thread is calling a web service appropiately, and does what it specifies?
Imagine being able to create a security system, and prove it can't be hacked, or if it can, know exactly how by proving which scenarios it can happen in?

I believe this all falls under proving program correctness, which devolves into the halting problem and "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." (Wikipedia)

[sepp2k]

gonzaw, on 06 November 2013 - 02:59 AM, said:

Another doubt I have is: Are there any OO languages, or maybe procedural ones, that have an extensive type theory similar to CTTs?

Try ATS. It's an imperative language that uses dependent types, linear types and other advanced type system features. Note that unlike Agda and Coq, ATS is Turing complete, so you won't be able to prove correctness with 100% certainty.

Quote

For some subset of programming, specially Functional Programming, this is already done with proof assistants like Agda or Coq. But that subset of programming isn't really practical.

I beg to differ.

Quote

I want it to be mainstream, I want it to be used everywhere, I want it to be applied to anything you could want programming applied to.

That's not realistic. Any language with the properties you're looking for will have to be way too verbose to be practical for anything where correctness isn't paramount. Even with aggressive type inference this can't be entirely avoided. Not to mention that the type system would be too complicated for many programmers to feel comfortable with.

Momerath, on 06 November 2013 - 07:32 AM, said:

I believe this all falls under proving program correctness, which devolves into the halting problem and "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." (Wikipedia)

Coq, Agda and similar languages are not Turing Complete and the Halting Problem is solvable for them (in fact they always halt). Generally if you want to verify programs, you have to choose between programming in a non-Turing complete language or having an unsafe subset of your language that can't be verified. However that hardly means that research in verification is not worthwhile.

PS: Sorry for the downvote - that was an accident.

[gonzaw]

sepp2k, on 06 November 2013 - 11:01 AM, said:

gonzaw, on 06 November 2013 - 02:59 AM, said:

Another doubt I have is: Are there any OO languages, or maybe procedural ones, that have an extensive type theory similar to CTTs?

Try ATS. It's an imperative language that uses dependent types, linear types and other advanced type system features. Note that unlike Agda and Coq, ATS is Turing complete, so you won't be able to prove correctness with 100% certainty.

Thanks I'll check it out

Quote

Quote

For some subset of programming, specially Functional Programming, this is already done with proof assistants like Agda or Coq. But that subset of programming isn't really practical.

I beg to differ.

Functional programming is practical, but I think mostly when it's embedded in another multi-paradigm language. A fully FP language on it's own isn't too practical. E.g I don't think I ever used a software program that said "this was written in Haskell" (other than maybe some Linux ones).

Quote

Quote

I want it to be mainstream, I want it to be used everywhere, I want it to be applied to anything you could want programming applied to.

That's not realistic. Any language with the properties you're looking for will have to be way too verbose to be practical for anything where correctness isn't paramount. Even with aggressive type inference this can't be entirely avoided. Not to mention that the type system would be too complicated for many programmers to feel comfortable with.

The theory itself can be as verbose as it wants. But surely you can create a compiler, IDEs, etc that allow you to create a very "simplified" language for any common programmer to use.
About the last point, it does feel like it'd need a paradigm change. But if done carefully I don't really see why it can't be possible (making people "comfortable" in this new system). Of course it'd take time, lots of training, slowly growing in the industry and being taught in courses, etc.

Quote

Momerath, on 06 November 2013 - 07:32 AM, said:

I believe this all falls under proving program correctness, which devolves into the halting problem and "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." (Wikipedia)

Coq, Agda and similar languages are not Turing Complete and the Halting Problem is solvable for them (in fact they always halt). Generally if you want to verify programs, you have to choose between programming in a non-Turing complete language or having an unsafe subset of your language that can't be verified. However that hardly means that research in verification is not worthwhile.

Yeah. Most easy example is that all recursion must end.
To be honest, unless I am shown an example of a problem a non-Turing Complete language can't solve, buta Turing Complete one can, and it's actually a problem I care about, I don't really care if the language is non-TC.
For instance, you can say something like "You can't create a Turing Machine compiler!" or something, but I don't really care about that type of problems (you can use any other Turing Complete language to solve that particular problem if you like), and I wouldn't really mind it not being solvable in this new "super" non-TC language.

I do believe there might be some instances it can't model, that you might want to model (a "while true" loop in a thread that handles events for instance). Maybe you won't be able to model it 100%, but any bit helps.
For "usual" problems like that, I think you could model them in another way, if you want to prove the program is correct, and include that new model in the language. For instance, you could create axioms and the like, that would model the kind of stuff you can't model in the language itself (like that "service offering" thread/process/etc).
That's what I want: Model as much as possible, and include it in the language. Be able to prove correctness of anything regarding that model. When you realize something is wrong, then you can easily pinpoint where the error is: It's not on the way the program works, it's not on the logic or the program itself, it's on that model you used as a base. You can easily use other tools, maybe even other languages to "fix" that problem, and then keep going on with the in-language-model.
Don't really know how to explain it better than that...but I think it could be a possible way to include program correctness verification into "everyday problems"


One example I can think of is a Web Service that fulfils a contract. You could have a SOAP WS, that tells you "if you give me X and Y, I will do Z". I doubt you could model that interaction, and the WS itself, in the language. But you could "assume" the WS fulfils its contract, and maybe give an alternative case where it doesnt (like those "Maybe X" from Haskell). With this modelled, you could then include that WS into your verification program, and maybe do stuff like "if I call the WS with parameters n and n/2, it will return n+2" and prove it.
I think you could do something similar to any other "unsolvable" problem you could find. Don't try to verify EVERYTHING is correct, but try to verify the most, and narrow down the places where errors can be made (i.e what's not verifiable), so if an error does happen, you can easily go there and fix it, instead of just knowing an error occurred somewhere and having no idea where it happened, why, etc (like you would in Black Box testing for example)