Validity & Veracity

I finally summoned up motivation to read The Annotated Turing by Charles Petzold. I bought the book in Jan2012. Ever since then it was a pending TODO. Now that I have time on my hands, I decided to attend to it while the grey cells were still active.

 From pg. 45. "In Hilbert's conception, the construction of a formal mathematical system begins with definitions, axioms, and rules for constructing theorems from axioms."

My Take:

• The regular expressions that are used by in the Lexical Analysis phase of the compiler are Definitions .
• The productions of the grammar rules, used in the Syntax Analysis phase, are Axioms. The output is an Abstract Syntax Tree (AST)
• Finally the Semantic Analysis phase is the one where the rules of the language are used to extract the operations that are implied by the AST. The output is an Intermediate Representation (IR). That is where the front end of a compiler ends. Subsequent steps are transformations to make the code execute on some CPU
• Thus the IR output of the compiler is a theorem constructed from axioms.
• The rules and axioms are coded in to the compiler.
• A compiler therefore qualifies as a formal mathematical system.
  
  

From pg. 46. " ... but the rules also imply the syntax of a well formed formula ... that is possible within the system. You can assemble a well-formed formula without first deriving it from your system, and then you can attempt to show that it's a consequence of the axioms by applying the axioms and rules in a proof."

My Take:

• When we write a program in a high-level language we in fact "assemble a well-formed formula without first deriving it from your system".
• Then when we successfully compile it we in fact show that "it's a consequence of the axioms by applying the axioms and rules in a proof"

From pg. 47. "Provability is a syntactic concept; it is based on the axioms of the system and the rules used to derive theorems. Truth, however, is semantic concept that depends upon the actual meaning we give to the symbols in the system."

My Take:

• Successful compilation proves Validity.
• Successful compilation does not prove Veracity (Truth).
• There is no getting away from well designed tests. Such tests are close approximations of a "proof" of Veracity.

Validation & Verification

Validity & Verity
I am asked. "Did you have lunch today?"

I answer, "Monday."

That answer is invalid. The question has just two valid answers - "Yes" or "No".

If I give one of the valid answers, it does not mean it is the truth (verity). My answer has to be verified.

Validation checks for Validity. Verification checks for Veracity.

Valid Programs & Correct Programs
A C program that can be compiled without errors is a valid C program. Is it a correct program? By executing the program, it can be verified that the program meets its specification. It can be verified that the program is correct. Correct programs are a subset of Valid programs.

Validation Criteria & Quality
What if the compiler options are set to treat all warnings as errors? Now if there are warnings the program will not compile. The program is no longer a valid program. There is nothing to verify.

What if, to successfully check-in code to the version control system, the code must meet Complexity Metrics?

What if the code cannot be checked-in because coding standards are not met?

There is more to qualifying as valid code than just clearing compiler errors.

If you want to improve code quality, enforce stricter validation criteria.