Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
764 lines (428 sloc) 19.2 KB

Going Back to the Future

A little history of programming to help explain why I like Kotlin, a 21st-century industrial language, using primary sources and first-hand experiments

Permalink


COMMENTARY:



- Coherence

Coherence Etymology


COMMENTARY: The root of the word is from the Latin for "to stick together". When you are going "to cohere", the objects begin separated and move closer to become "one". I would like to highlight the gap between computational problem solution and programming language design, especially from a historical perspective. Despite significant inertia over the decades, the long-term trend is to close this gap.



- Shorten the conceptual gap

... our intellectual powers are rather geared to master static relations and that our powers to visualize processes evolving in time are relatively poorly developed. For that reason we should [...] shorten the conceptual gap between the static program and the dynamic process, to make the correspondence between the program (spread out in text space) and the process (spread out in time) as trivial as possible.

Go To Statement Considered Harmful


COMMENTARY: Djikstra's famous letter provides our first example of a coherence problem, where the static text and the dynamic execution are conceptually separated, making understanding and reasoning about the program more difficult."



- JDK download

http://www.oracle.com/technetwork/java/javase/downloads/jdk8-downloads-2133151.html

COMMENTARY: As expectations increase about how much computers can do and how fast they do it, there will be increased demand for distributed processing, at both the hardware and system level. Languages and runtimes that rode the rise of HTTP will eventually give way to faster environments. Currently, the Java Virtual Machine has the greatest mindshare, broadest application, best performance, most maturity and planning of the contenders. As a host for new and future languages, it holds the most promise, despite some of its legacy short-comings.

According to Human Benchmark, the average reaction time is 215 ms. That's the window you have for apps with a human user to seem quick. It may be worth differentiating "premature optimization" from accommodating actual human neuron timescales.



- Intellij download

https://www.jetbrains.com/idea/download

COMMENTARY: Kotlin will run in other development environments, but the experience is much more pleasant in Intellij.



- Manchester Small-Scale Experimental Machine

June 21, 1948 - Program runs successfully on first binary, digital, electronic stored-program computer (in which data and instructions are stored in same memory)



- First successful "stored" program (Manchester SSEM)

Highest proper factor; uses subtraction instead of division



- Highest proper factor (attempt #1)

fun main(args: Array<String>) {
	val input = 12
	var remainder = input
	var factor = input - 1

	while (factor > 1) {
	while (remainder >= 0) {
		if (remainder == 0) {
		println(factor)
		return
		}
		remainder = remainder - factor
	}
	remainder = input
	factor--
	}
}
  • No annotations of type; they are "inferred"
  • val is unchangeable
  • var is destructive assignment; value is destroyed elsewhere
  • 'remainder' is not remainder at first; Englishy naming not that helpful
  • Nested println modifies state in the environment, not in the program/algorithm
  • Nested return is a jump (ie GO TO)
  • Statement nesting leads to conceptual gap that has to be jumped over

But is it correct?



- Accepted methodology ... find more bugs and make more patches

The accepted methodology for program construction was [...]: People would write code and make test runs, then find bugs and make patches, then find more bugs and make more patches, and so on until not being able to discover any further errors, yet always living in dread for fear that a new case would turn up on the next day and lead to a new type of failure

Robert W Floyd, In Memoriam by Donald Knuth

Video of Knuth talking about Floyd



- Function (extensional)



- Domain, Co-domain, Range



- ENIAC

Electronic Numerical Integrator and Computer (ENIAC)



- Presper Eckert & John Mauchly

Disclosure of Magnetic Calculating Machine



- First Draft of a Report on the EDVAC

... a really high speed device would be very limited in its usefulness unless it can rely on M [ie, Memory], rather than on R [ie, I/O], for all the purposes enumerated in 2.4, (a)–(h) [ie, Calculation]

First Draft of a Report on the EDVAC


Julian Bigelow, Herman Goldstine, Robert Oppenheimer, John Von Neumann


Max Newman



- Guerilla Open Access Manifesto

Providing scientific articles to those at elite universities in the First World, but not to children in the Global South?

Guerilla Open Access Manifesto


Aaron Schwartz



- Coding is not a static process of translation

Thus the relation of the coded instruction sequence to the mathematically conceived procedure of (numerical) solution is not a statical one, that of a translation, but highly dynamical ... (p.2)

Our problem is then to find simple, step-by-step methods, by which these difficulties can be overcome. Since coding is not a static process of translation, but rather the technique of providing a dynamic background to control the automatic evolution of a meaning, it has to be viewed as a logical problem and one that represents a new branch of formal logics. (p.2)

We now proceed to analyze the procedings by which one can build up the appropriate coded sequence for a given problem — or rather for a given numerical method to solve that problem. As was pointed out in 7.1, this is not a mere question of translation (of a mathematical text into a code), but rather a question of providing a control scheme for a highly dynamical process, all parts of which may undergo repeated and relevant changes in the course of this process. (p.4)

We therefore propose to begin the planning of a coded sequence by laying out a schematic of the course of C through that sequence, i.e. through the required region of the selectron memory. This schematic is the flow diagram of C (p.4)

Planning and Coding of Problems for an Electronic Computing Instrument

https://library.ias.edu/files/pdfs/ecp/planningcodingof0103inst.pdf



- Assigning Meanings to Programs

The basis of our approach is ... an association of a proposition with each connection in the flow of control through a program.

https://classes.soe.ucsc.edu/cmps290g/Fall09/Papers/AssigningMeanings1967.pdf



- Highest proper factor (as pseudo-assembly)

	   n ∉ ℙ  (where ℙ is the set of prime numbers)
	1. r ⟵ n
	2. f ⟵ r - 1
INNER:  3. if (r = 0?) goto EXIT
OUTER:  4. if (f = 1?) goto NEXT
	5. r ⟵ r - f
	6. goto INNER
NEXT:   7. f ⟵ f - 1
	8. r ⟵ n
	9. goto OUTER
EXIT:  10.
  • Pseudo-assembly inspired by Hing Leung "Program Correctness" project http://bit.ly/2xrshIW
  • Goal makes sense only for particular input set (non-Prime numbers)
  • Termination condition moved to the outside
  • Structured loops (ie while) become conditional jumps
  • Loops are book-ended by two gotos
  • Loop check is inverted from original structured version


- Highest proper factor (as flow chart)

Flow Chart

  • TODO add assertions
  • The starting and ending assertions are assumed to be true. The "program proof" is the assertion sequence in between.
  • Proof of termination is separate from "partial completeness" proof
  • Chart done in draw.io


- Highest proper factor (attempt #2)

fun main(args: Array<String>) {
	val input = 12
	var remainder = input
	var factor = input - 1

	loop@
	while (factor > 1) {
	while (remainder > 0) {
		remainder = remainder - factor
	}
	if (remainder == 0) break@loop
	factor--
	remainder = input
	}

	println(factor)
}
  • Jump on terminating condition
  • Output moved to boundary with environment
  • Domain is incorrect; results in '1' for prime numbers


- Axiomatic Basis

Computer programming is an exact science in that all the properties of a program and all the consequences of executing it in any given environment can, in principle, be found out from the text of the program itself by means of purely deductive reasoning.

An Axiomatic Basis for Computer Programming


Tony Hoare



- Greatest proper factor (attempt #?)

(annotated with assertions)

TODO



- I have only proved it correct

Beware of bugs in the above code; I have only proved it correct, not tried it

The Correspondence Between Knuth and van Emde Boas


Don Knuth



- GPF (attempt #? wrapped in subroutine)

fun gpf(input: Int): Int {
	var remainder = input
	var factor = input - 1
	loop@
	while (factor > 1) {
		while (remainder > 0) {
			remainder = remainder - factor
		}
		if (remainder == 0) break@loop
		factor--
		remainder = input
	}
	return factor
}


- GPF Automated tests

class GPFKtTest {
	@Test
	fun checkGPF12() {
		assertEquals(gpf(12), 6)
	}
	@Test
	fun checkGPFKilburn() {
		assertEquals(gpf(262144), 131072)
	}
	@Test
	fun checkGPFPrime() {
		assertEquals(gpf(13), 1)
	}
}


- Cyclomatic complexity

How to modularize a software system so that the resulting modules are both testable and maintable?

A Complexity Measure



- A program ...

A FORTRAN source program consists of a sequence of FORTRAN statements (p7)

The Automatic Coding System for the IBM 704 EDPM

In IPL a program ... is a system of subroutines ... organized in a roughly hierarchical fashion. (p16)

Programming the Logic Theory Machine


COMMENTARY: Mark Priestly compares the history of the two approaches in

AI and the Origins of the Functional Programming Language Style



- Symbolic computation

...whenever numbers meaning operations and not quantities ... It might have been arranged that all ... numbers meaning operations should have appeared on some separate portion of the engine from that which presents numerical quantities (p16)

The operating mechanism can even be thrown into action independently of any object to operate upon .... Again, it might act upon other things besides number (p17)

Sketch of the Analytical Engine


Ada Lovelace


Lovelace arguably anticipates Gödel's use of numbers to represent logical propositions

The basic signs of the system P are now ordered in one-to-one correspondence with natural numbers (p45)

On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Original German

Note also that Gödel introduces a notion of computability using recursive functions.



- An entirely different kind of power ... the ability to do recursions

An entirely different kind of power arises from the flexibility of the hierarchy -- the ability to do recursions. An instruction may be used in its own defining subroutine, or in any of the subroutines connected with its definition, in any way whatsoever provided that the routine does not modify itself and that the entire process terminates. (p34)

Programming the Logic Theory Machine



- Conditional expression

The object of this note is to advocate that the IAL language be extended to include two additional additional notations: conditional expressions and recursive definitions

( p₁ → e₁, ..., pₓ → eₓ )
gcd(m,n) = (m > n → gcd(n, m),
	   rem(n,m) = 0 → m,
	   T → gcd(rem(n,m), m))

Letters to the Editor, Communications of the ACM, I no.12 1958

You have to pay $15 to read this one-page letter.

John McCarthy



- Greatest Common Divisor with Conditional Expression & Recursion

// McCarthy's algorithm
fun gcd(m: Int, n: Int): Int =
	if (m > n) gcd(n, m)
	else if (n % m == 0) m
	else gcd(n % m, m)
// Euclid's algorithm
fun gcd(m: Int, n: Int): Int =
	if (m % n == 0) n
	else gcd(n, m % n)


- Greatest proper factor (attempt #?)

fun main(args: Array<String>) {
	val input = 12

	val result = checkFactors(input, input - 1)

	println(result)
}


fun properFactor(remainder: Int, factor: Int): Boolean {
	return if (remainder > 0) properFactor(remainder - factor, factor)
	else remainder == 0
}


tailrec fun checkFactors(n: Int, trial: Int): Int {
	return if (properFactor(n, trial)) trial     // is trial a proper factor of n?
	else checkFactors(n, trial - 1) // if not, reduce trial and try again
}




- An Algebraic Language

1.1.1 Manipulating sentences in formal languages ...

1.1.2 The formal processes of mathematics such as algebraic simplification, formal differentiation and integration ...

1.1.3 A compiler ... except for input and output ...

1.1.4 Heuristic programs ...

1.1.5 ... representing expressions whose number and length may change ...

An Algebraic Language for the Manipulation of Symbolic Expressions



- map

maplist[x;f]
The function maplist is a mapping of the list x onto a new list f[x]

maplist[x;f] = [null[x] → NIL;
		T → cons[f[x]; maplist[cdr[x];f]]]

(p122)

LISP I Programmer's Manual



- ISWIM

ISWIM is based on LISP but is more regular and in some ways more convenient. It may best be regarded as a palatable syntactic dress for Church's lambda calculus, and the ... known logical properties makes it suitable for us here.

let rec concat(xs1,xs2) =
   if null(xs1) then xs2
   else let x = car(xs1) and xs3 = cdr(xs1)
   cons(x, concat(xs3,xs2))

Proving Properties of Programs by Structural Induction

The Next 700 Programming Languages

// not idiomatic Kotlin
fun <T> concat(xs1: List<T>, xs2: List<T>): List<T> =
	if (xs1.isEmpty()) xs2
	else {
		val x:T = xs1.head()
		val xs3 = xs1.tail()
		listOf(x) + concat(xs3, xs2)
	}

Peter Landin



- Record Handling

Problems involving structured data arise in many areas of computer application ...

All the relationships introduced above ... are in fact partial ... In order to meet this problem, a special null value is provided for reference variables and fields.

Record Handling

Notes on Data Structuring



- Records in Kotlin

TODO



- Missing references - another way

... my friend, Edsger Djisktra, thought the null reference was a bad idea

If you have a null reference, then every bachelor who you represent in your object structure will seem to be married polyamorously to the same person, Nulla

I did know that there was a solution to this problem based on the idea of discrimination of objects belonging to a disjoint union class

Null References: The Billion Dollar Mistake



- Optional

TODO



- Null in Kotlin

TODO



- Propositions as Types

The Formula-As-Types Notion of Construction



- Abstract types

(hide implementation)

TODO



- CLU

TODO

Barbara Liskov (with Jack Dennis)



- Algebraic specification



- Kotlin dependencies

// build.gradle

dependencies {
	compile "org.jetbrains.kotlin:kotlin-stdlib-jre8:$kotlin_version"
	testCompile group: 'junit', name: 'junit', version: '4.12'
}


- Random testing against algebraic specifications