# Programming and Logic, past and future

Menu Menu

## 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 NetworkSoftware

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 somethingx is a some kind of things

f xf 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 -> Bb is an element of B

b : B

## Lambda calculus with types

assuming b : B.

f : A -> B f = λ ( x : A ) -> bassuming 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 → SpecificationIf ¬ (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

## implications

## disjunctions

## conjunctions

## system T

## 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