7 kyu
Google interview
59 of 318ice1000
Loading description...
Theorem Proving
Data Structures
Trees
Algorithms
View
This comment has been reported as {{ abuseKindText }}.
Show
This comment has been hidden. You can view it now .
This comment can not be viewed.
- |
- Reply
- Edit
- View Solution
- Expand 1 Reply Expand {{ comments?.length }} replies
- Collapse
- Spoiler
- Remove
- Remove comment & replies
- Report
{{ fetchSolutionsError }}
-
-
Your rendered github-flavored markdown will appear here.
-
Label this discussion...
-
No Label
Keep the comment unlabeled if none of the below applies.
-
Issue
Use the issue label when reporting problems with the kata.
Be sure to explain the problem clearly and include the steps to reproduce. -
Suggestion
Use the suggestion label if you have feedback on how this kata can be improved.
-
Question
Use the question label if you have questions and/or need help solving the kata.
Don't forget to mention the language you're using, and mark as having spoiler if you include your solution.
-
No Label
- Cancel
Commenting is not allowed on this discussion
You cannot view this solution
There is no solution to show
Please sign in or sign up to leave a comment.
This comment has been hidden.
Note to moderators: This Kata is not yet ready for re-approval. Its current average assessed rank is
5 kyu
but we need to bring it down to8 kyu
(or at most7 kyu
) before it can be considered for re-approval.See: Codewars/codewars.com#2001
Changed estimated rank into
7 kyu
.This comment has been hidden.
Fixed.
That's not really a proof of correctness though.
I was pondering about program correctness too, and I came to the conslusion that it's a subjective term, so we can only pove that our program behaves according to a formal specification but can never prove that "its bug free" whatever that means. So my thinking is that there is no such thing as proof of correctness, until we can formalize "correctness" which we can't.
You might be interested in this renewed attempt to establish the correctness of binary tree inversion ;-)
Coq translation
Approved
Agda translation
Approved