Programming and Logic, past and future

Shinji KONO

What is reliabilty?

    Keeping secrets are very small part of security.
    System must keep working
        high availability
        correctly working
    System may fail (ex. hardware failure, fire) 
        Backup is important
    Accessibility
        Unusable system is the most safe one?
        compromise ( such as 4 digit password)
    Human factor
        Technology itself does not make the system reliable
        be a reliable person

Risks and reliablities

    Risks varies ...
        light or serious
        rare or frequent
        predictable or unpredictable
    Reliablities are relative to
        specifications
        predections

Security vs ...

    Security vs Usability
    Security vs Costs

Is human reliable?

    Keep working?
    Working safely?
    It is available?
    It works even in an extreme condition?

A hardware or a software satisfies specification

Hardware

    Finite automaton ( looping on fix amount of state, very simple)
    CPU
    Memory 
    Network

Software

    Operating system Application
    Services
    Framework
    Library
    Database

Reliabilties of programs

    Program is written in programming languages
    Program do something depends on inputs, environment or non-determinism
    Program have to keep requirements

What is a requirement?

    Mathematical relations of inputs and outupts
    These are written in logics

History of logic

Logic describes relations of properties. At first, these are written in a natural language such as English or Japanese.

Philosophers (such as Euclid) separate assumptions and consequences. Theorems (Consequences) are inferred from Axioms (assumptions).

Frege deines theory of descriptions as a formal language which is not a natural languages. It contains predicate and connectives.

  Value:     name of some concrete things
  Variable:  name assuming contains some value
  Predicate: pair of predicate name and arguments, which may true or fale
  Connectives:  negation(not), disjunction(or), conjunction(and)
  Qunatifier:  ∀ for all ,  ∃ exists

Logic is mathematics now

  rule of manipulating symbols, which is a seriales of characters
  Term rewriting system (lambda calculus)

lambda calculus

  syntax definition
  rewriting rule

syntax of lambda calculus

   a,b,c       constant
   x,y,z       variable
   a           constant is a term 
   λ x -> X    is a term if we have a term  X
   f a         function f and it's an argument a

rewriting rule of lambda calculus

   ( λ x -> f x )  a
  -----------------------
       f a

What is a variable? What is a type?

   x contains something

x is a some kind of things

f x

f does not accepts all possible things, but it accepts some kind of thing such as an element of Set A. f returns some kind of things such as an element of Set B.

   f : A  -> B

b is an element of B

   b : B

Lambda calculus with types

assuming b : B.

   f : A -> B
   f = λ ( x : A ) -> b

assuming a : A , type of f a is B.

   lemma1 : B
   lemma1 = f a

Specification is described in logics

    if P then Q
    (¬ P ) ∨ Q
    every time P is happen, Q will be true
    □ ( P → ◇ Q )

Specification / Implementation / Execution

    Specification in logic
    Implement in functions
    Execution result is set

First order logic

    p          p is true
  　¬ p        p is not true
    p ∧ q      p and q is true
    p ∨ q      p or q is true
    p → q      p implies q ( ¬ p ∨ q )

formula and it's meanings.

    value of variables
    assert
    all assertions are correct (valid)
    in any permutated executions

Temporal Logic

    □p      always p
    ◇p      sometimes p
    ◇p = ¬ □ ¬ p

How do we handle specifications

    Implemenation → Specification

If ¬ (Implemenation → Specification ) is satisfiable, there is a bug.

    →  Model checking  (SPIN / Java Pathfinder )

Or we can prove ( Implemenation → Specification ) directory

    →  Proof assistance ( Agda )

Proof system

Proofs in a first order logic is an function ( lambda calculus)

Write down the proofs as a function

    Coq
    Agda

Curry Howard Isomorphism

Logic formula is a type. Proof is a lambda function.

    type-name : type
    type-name = proof as a lambda term

    Interaction with outside or environments
    handling very large implementation and spefication in logics

What are we doing?

    Continuation based C (CbC)  ( more primitve C language )
    Implement Operating system on CbC 
    Provide model checking and proof system for CbC