5 ms·
This is a cool thing. I've been thinking about this with functions, and trying to think of a way to make a programming language have support for a proof checke
by drdeca 11y ago
This is a cool thing.
I've been thinking about this with functions, and trying to think of a way to make a programming language have support for a proof checker for this sort of thing built in, with functions having pre and postconditions, and function bodies that prove the postcondition is true after the function is run, given that the precondition was true before it was run, but I've encountered a problem when one allows first class functions.
If one allows first class functions, it seems that it would allow one to make tricks like "if this statement is true, 2+2=5". I'm not sure how to get around it.
It's possible that if one actually tried what I am thinking would be the problem, the preprocessor-thing (the thing that validates all the proofs before the program is actually run as a program) might just get into an infinite loop (through infinite recursion).
But it doesn't look like that would necessarily happen.
And I'm not sure what thing in what I've written should be something that the proof validator should accept, but it certainly does not seem like the proof validator should accept all of it (because it can be used to "prove" anything that can be expressed in the language)
- ahelwer 11y agoLook at the Dafny language from MSR: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ Your problem is, I think, assuming programs have correctness as an intrinsic property. This is not so. Programs can only be correct with respect to something - some idea born in a human mind, transcribed into something the checker understands (here, pre- and post-conditions). If the human mind wants 2+2 to equal 5 in their program, all power to them - they must only ensure this does not cause inconsistency.
- mcguire 11y agoShould I be concerned that the Dafny tutorial (http://rise4fun.com/Dafny/tutorial/guide http://rise4fun.com/Dafny/tutorial/guide) seems kind of...odd? Getting Started with Dafny: A Guide 1. undefined 2. undefined 3. undefined ...
- tikhonj 11y agoYou might be interested in the YNot[1] project, which is a library implementing Hoare-style axiomatic semantics in Coq. Just using Coq as the proof language answers a lot of your questions since Coq has well-understood limitations designed to make it useful for automatic proofs. If you're not familiar with the idea of dependent types, it's definitely worth learning about them (and Coq is a good place to start) because they formalize the idea of arbitrary functions at the type level by letting types depend on values, giving you the ability to verify whatever invariants you like. A good place to start would be Benjamin Pierce's free Software Foundations[2] book. There's a really rich theory here with a lot of both theoretical and practical problems worked out but, at the same time, lots of room to develop new ideas and approaches if this is something you're interested in. [1]: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ [2]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html