Anonymous user
Talk:Proof: Difference between revisions
→The Go proof?: new section
Underscore (talk | contribs) (→Proofs) |
(→The Go proof?: new section) |
||
Line 25:
:::: I passed Calc 2, and it ''still'' took me a couple years and lurking in discussions of C++0x before I really started understanding what was being talked about in this task. Type theory and calculus seem to me to be orthogonal subjects. --[[User:Short Circuit|Michael Mol]] 19:19, 6 November 2009 (UTC)
:::: Rightly or wrongly, elementary calculus is in most colleges a ''prerequisite'' for courses on basic proof-writing. I'm a math major and I ended up taking vector calculus before "foundations of mathematics". —[[User:Underscore|Underscore]] 20:34, 6 November 2009 (UTC)
== The Go proof? ==
The Go sample seems questionable. It claims that successful compilation completes the proof, but what if I make some small changes to the code?
<lang Go>var zero number = e0.pn // see axiom 5, below.
var one = zero.successor() // I added this
....
func (s *evenPeano) hasEvenSuccessor() (even, bool) {
// if s.normalize() == zero { //original code
if s.normalize() == one { //I added this
return nil, false
</lang>By the way, all the "has*Successor" probably should have been named "hasPredecessor" instead. Anyway, by the proof's logic, what was evenPeano is in fact "oddPeano" now, and it still compiles fine. Does that just prove sum of two odd numbers are also odd numbers? --[[User:Ledrug|Ledrug]] 20:46, 21 June 2011 (UTC)
| |||