1TODO Introduction?

It would be nice if software engineering had predictive theories like Newton's laws of motion.

[1]

Software science is a study of software. But what is software? See file:software.html.

2What do we want to predict?

The creation of a branch of science begins with the desire to understand, explain, and predict something (the object of study). For example, humans wanted to predict the motion of objects, and thus mechanics was born.

Why are things easy or difficult to predict? Why is it easy to predict where a planet will be in years, but it is hard to predict what I want? The difficulty of predicting something depends on the number of factors that influence that thing.

We want to predict the amount of effort required to create a piece of software, because we want to predict how long it takes to make a piece of software.

We want to predict the number of users a software system can serve simultaneously.

Software is exploration. The only know whether a library suits our needs is by actually trying it out, by using it for our use cases.

Instead of trying to make a perfect library that foresees all future scenarios, we should make it easier to modify libraries. The biggest hassle in modifying libraries is fetching the transitive closure of their dependencies, dealing with their idiosyncratic build systems, and maintaining a patch. Then the library users hope that the library author is competent and empathetic and does not gratuitously break backwards-compatibility.

3Why do we want to change software?

Software is a model of reality. Thus software change reflects a change in reality that invalidates the software's axioms or simplifying assumptions.

Software will not change if reality does not change.

For example, ID card numbering schemes changed, the set of genders changed, tax laws changed.

4Software science

4.1What is the science of software engineering?

If a branch of engineering is an application of a branch of science, then what branch of science is applied in software engineering? What is software science?

Civil engineering is the application of natural science (especially physics) to build civil structures such as bridges, buildings, dams, roads, and other many things used by civilizations.

A civil engineer can predict how much load a steel beam can handle. Can a software engineer predict how much load a machine can handle?

Software engineering is the application of computer science?

2018 slides "What would a science of software engineering look like?"1

4.2Mathematics as a domain-specific language for science?

Mathematics is more like a domain-specific language than a branch of science. Mathematics is a language optimized for abstract thinking?

4.3Where is software science?

https://ubiquity.acm.org/article.cfm?id=2590529

https://services.math.duke.edu/undergraduate/Handbook96_97/node5.html

The abstract-object counterpart of concrete-object physics How do we apply the scientific method to the study of abstract objects? To anything?

If engineering is an application of science, what is the science that is applied in software engineering?

We need something like Newton's laws of motions for software dynamics that will enable us to predict things.

What should be the object of study of software science? Software? What is software? A model of reality? A model.

Software dynamics? Science of bottlenecks? Queuing theory.

If computer science is science, where are the falsifiable theories and the experiments?

A software is a model of reality.

Which branch of science studies models?

Which branch of science studies abstract objects? None. All branches so far are materialistic. They study concrete objects.

What experiments can be done with abstract objects? Besides thought experiments?

We can experiment with a program: We can stress-test it to figure out its maximum load (the maximum number of requests it can handle per second without errors), in a similar way we stress-test a steel bar to figure out its maximum load (the maximum force it can withstand without breaking). Benchmark games are similar to tables of material strengths.

We can experiment with abstract objects. For example, we can test software, we can test ideas. The problem is that each piece of software creates its own branch of science that is not transferable to other pieces of software. For example, knowledge of word processors is not applicable to accounting information systems. It is as if there were different Newton's laws of motion for cars, bikes, rocks, and other things. We need a science of all software, not just a particular software.

What does science do with its object of study? Come up with a predictive theory and experiments to falsify it.

Science comes from Latin "scientia" which simply means "knowledge", but "science" is the application of the scientific method, the formulation of theories with explanatory and predictive power, and the experimentation to falsify such theories.

Before science can even exist, the language must first exist. We must first invent the terms, name the objects, and form the ontology. We must first find out what to talk about. We must first define the object of study.

4.4Why has mathematics not revolutionized biology or software engineering?

Is it due to the nature of biology or software engineering?

Or I don't know that it has?

https://www.ams.org/notices/201510/rnoti-p1172.pdf

4.5The object of study

The object of study may be software itself, or an aspect of software, such as requirements, capacity, complexity, performance.

4.6Good laws, enforceability, and unintended consequences

Good laws are:

  1. enforceable, and
  2. have minimal unintended consequences.

Human laws are programs executed by humans. The nature of human laws is the same as computer programs, The difference is that humans mostly follow the spirit of the law, and computers always follow the letter of the law.

Example: Banning smoking is not practical to enforce: Are you going to put a cop in each building? Banning prostitution is not enforceable: Are you going to put a cop in each building?

I hypothesize that the principles of good software engineering is applicable to good legal engineering. Lawmakers are legal engineers. They should have engineering background. They engineer the lives of lots of people and the future of nations.

5Subfields of software science?

5.1Turing?

Turing's theory is about computation, not software.

5.2Software complexity theory

Essential complexity = Kolmogorov complexity = the length of the shortest description of the software. The description must contain enough information for clean-room-reimplementation by another software engineer without any communication to the requirement analyst.

Accidental complexity = a measure of the apparent size of the software; number of syntax objects (abstract-syntax-tree nodes), number of lines of code.

5.3Essential complexity theory

Here we are interested in a measure of complexity, the cognitive load of understanding the software?

Kolmogorov complexity.

The complexity of a software system is the length of the shortest description of that system. The description must be such that someone else can recreate the system from only the description.

Example: a formula that describes a program that checks whether a list \(x\) is ordered according to the ordering \(\le\).

\( \forall i \forall j ( i \le j \implies x_i \le x_j ) \)

The formula can then be fed to descriptive complexity theory in order to determine the minimum possible resources required to implement the system. For example, it is a well-known fact in computer science that comparison-sort of an array of \( n \) elements require \( \Omega(n log n) \) time.

If something takes \( t \) seconds to finish, then doing it \( n \) times takes \( n \cdot t \) seconds to finish.

That should also work under uncertainty: If something takes \( t \) seconds to finish on average, then doing it \( n \) times takes \( n \cdot t \) seconds to finish on average. But telling the whole truth requires knowing the shape of the distribution, not only the mean.

5.4Descriptive complexity theory

Descriptive complexity theory is deep: It puts a lower bound on the solutions of problems regardless of the machines that implement those solutions. It is due to the inherent/essential complexity in logic itself, and not due to accidental complexity of the machine implementation.

In software engineering, the results of computational complexity theory are used for capacity planning, for example, that the lower time bound of comparison sorting is quasilinear2. This enables us to calculate the number of processors and the amount of memory, from the number of requests we expect to serve.

In reality, what is important is the actual number of seconds that users are willing to wait for computations with expected input sizes.

5.5Capacity planning theory

The mathematics of basic bottleneck science is simple: It is only basic arithmetics (addition, subtraction, multiplication, and division). If one wants more details, one can resort to queuing theory, but capacity planning can be done with simple basic arithmetics, without the full power of queuing theory3.

5.6Programming science

Lambda calculus can be a model of computer programs, but how do we experiment, and what should we falsify?

5.7Software development science

Software engineering is hard because it requires the engineer to estimate estimations.

We often want to estimate how long it takes to implement something.

But the estimation itself can only be done by doing the thing, because software development is full of unforeseeable roadblocks, because that software does not fit in our working memory. (How do we know that a library cannot do something? We have to try and find it out the hard way. Unfortunately that's the only way.)

So we try.

Thus we estimate how long it takes us to come up with a probable estimation.

Thus software engineering is second-order estimation.

Example: To estimate how long it takes to do X:

  • Try doing X for a week.
  • See how much is actually done.
  • Extrapolate.

This estimation should be much more accurate than pure guessing.

Thus the proper answer to "How long will it take?" is "It will take a week for me to come up with an estimation."

We estimate that it will take us a week to come up with an estimation.

It's hard to estimate how much time is required to implement something, because we need to estimate how long it takes to estimate.

The only known way to estimate software development time is by extrapolating: Try developing it for a month, measure the accomplishments, and extrapolate from there.

Is it simpler in civil engineering? If you know that laying one brick takes 10 seconds, then you know that laying 1,000 bricks takes 10,000 seconds, but that is an oversimplification: Some civil engineering projects are also late, such as Jakarta mass rapid transport, but is it a political issue or an engineering issue?

5.8Specification theory

A specification is a logical formula in conjunctive normal form with at least one positive clause (literal?).

5.9Science of models

How do we measure a model's quality/fidelity, and with respect to what purpose?

5.10Science of software changes

It is obvious that software has inertia, and bigger software is harder to change.

Suppose that we have a system \( S \) that satisfies the logical formula \( \phi \), and we want to change \( S \) to \( S' \) that satisfies \( \phi' \). How much is the effort? It seems that the effort cannot be deduced from the logical formula alone.

It is possible to make two programs that satisfy the same logical formula (have the same observable behavior) but have widely different source codes.

5.11States

All practical systems have memory.

All systems that have memory are stateful.

Thus, we have to learn to live with states.

5.12Human aspects

Complexity increases the probability of mistakes/disasters due to a mismatch between human mental models and the actual reality.

Examples4.

5.13Parsing theory

5.14Learning theory

6Logic

How do we measure the size of logical formulas?

7How do we write correct software?

7.1What is correct?

Correct with respect to what? It does what we want, and it only does what we want?

7.2Proving and testing

Testing approximates proving. We actually want to prove a logical formula phi about a piece of code, we want to prove that the code fragment is a model of the formula phi, but proving is too expensive. Therefore, we test phi instead.

In back-end testing, the formula is often obvious. What is the formula in front-end testing? DOM element existence testing?

7.3The problem with formal methods: you can't prove what you don't model.

7.3.1What if it is impossible to write correct software? What are our options to mitigate/limit the damage?

7.4What?

7.5Coq?

7.5.1Introduction

Coq source file extension is .v.

The notation x:T means "the type of x is T", "x inhabits T". It also means "x is a proof of T" by Curry-Howard isomorphism.

The type of nat is Type(1).

The type of set is Type(2).

The type of Type(i) is Type(i+1).

(* This is a comment in Coq. *)

coqtop -l filename.v -batch

7.5.2Defining things

Definition x: nat := 0.
Check x.

Definition f (x: nat): nat := x + 1.

Definition = non-recursive definition

Fixpoint = recursive definition

Inductive = type (Set (small set)) definition

Definition name: type
where
type: Set
or type: Prop
or type: Type.

Proving 0+1 = 1 using Curry-Howard isomorphism?

Axiom: and-elimination

\[\begin{align*} a \wedge b \vdash a \end{align*} \] 
Theorem and_elim: forall a b: Prop, a /\ b -> a.
tauto.
Qed.
\[\begin{align*} a \vdash a \vee b \end{align*} \]

Modus ponens

\[\begin{align*} a, a \rightarrow b \vdash b \end{align*} \]

7.5.3How Coq represents propositions

Print False.
Print True.
Inductive True : Prop := I : True.
Inductive False : Prop := .
Inductive and (A B : Prop) : Prop := and : A -> B -> and A B.

7.6Testing

Why do we test? Because we are not sure that our program is correct.

Why are we not sure that our program is correct?

  • Because we don't know how to prove its correctness. This can be alleviated by using a decent programming language.
  • Because the cost of proving its correctness does not justify the benefit. We can't do anything about this if the complexity is essential (irreducible), not accidental.

We human are fallible. Thus we will always test. Therefore:

  • What should we test?
  • How should we test?
  • What is the test that has the greatest benefit-to-cost ratio?

The expected benefit of a test is the expected cost of the mistakes that might have been made if the test did not exist.

The quality of a test is the seriousness of the mistakes it prevents. Thus, the seriousness of testing is proportional to the seriousness of risk.

Test is insurance. A good insurance covers your risk. A bad insurance only wastes money and doesn't cover your risk: Testing Java class getters is like buying flood insurance for a house in the desert.

Insurance causes moral hazard (taking more risk because someone else pays for it). Does having a test cause you to take more risks?

  • The benefit of a test is the cost of the mistakes it prevents.
  • The cost of a test is the person-hours spent writing the test and updating the test, and a slight increase in build time. (Assume $50/person-hour for simplicity.)

The answers to these questions tell us what to test and how to test:

  • What tests have the greatest benefit-to-cost ratio?
  • What mistakes do our tests prevent? How expensive are the mistakes that our tests prevent?
  • Which part of our code is most likely to cause expensive mistakes? (Example: testing getters won't prevent expensive mistakes.)

Code coverage is a meaningless metric. We should measure the expected value of mistakes instead. We should "color" our code: color more risky methods more red, color less risky methods more green, like this travel risk map5 but for software.

If you are launching a rocket, then a mistake may cost billions of dollars. It makes sense to invest ten million dollars testing to avoid a 1/100 probability of making a billion-dollar mistake.

7.7Symbolic execution

Chris Meudec67. Prolog constraint solving for C/Java testing.

7.8Model checking

Suppose that we have just written a function that sorts an array, and a mistake will cost $1,000,000. How do we prove that the function indeed sorts an array?

Clarke's overview and lots of examples in the 1990s http://www.cs.cmu.edu/~emc/15-398/lectures/overview.pdf

8Why does software have security holes?

Software has security holes because:

  1. Languages makes it too hard to do the right thing.
  2. Programmers are too lazy to do the right thing.

Authentication systems such as OAuth are too complex for programmers to use or understand. Anything more than HTTP Basic Auth is too complex. It sucks to write code for handling authentication. How do we make a programming system such that handling authentication is not hard? What is authentication and authorization?

"A Taxonomy of Causes of Software Vulnerabilities in Internet Software" https://pdfs.semanticscholar.org/5ec6/93950d1e6039e04a7b86a488e816ddcdd82e.pdf "software developers are making the same mistakes over and over again"

[1] Gries, D. 2012. The science of programming. Springer Science & Business Media. url: <http://www.cs.cornell.edu/gries/July2016/The-Science-Of-Programming-Gries-038790641X.pdf>.

  1. http://herbsleb.org/web-pres/slides/crowd-chase-2018-final-dist.pdf↩

  2. <2019-08-11> https://en.wikipedia.org/wiki/Time_complexity#Quasilinear_time↩

  3. https://en.wikipedia.org/wiki/Queueing_theory↩

  4. <2019-08-12> https://monzo.com/blog/2019/09/08/why-monzo-wasnt-working-on-july-29th↩

  5. https://i.redd.it/ktop13ad2io01.png↩

  6. http://tinyurl.com/y42eyfkp↩

  7. http://www.echancrure.eu↩