# 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

## What is comming next?

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

Shinji KONO / Mon Jan 29 16:06:21 2018