Soundness of Programming Languages

Soundness and Completeness at the Programming Language Level

Soundness in programming languages is a concept that represents the stability and reliability of a language's type system.

In other words, if a language's type system can catch all type-related errors in a program, the language is said to be "sound."

This serves as a measure of the safety and correctness provided by the programming language, helping programmers write safer code without runtime errors.

The Meaning of Soundness

Type Safety

Guarantees that no type errors will occur when the program is executed.

For example, it prevents runtime errors by detecting at compile time errors such as assigning a string to an integer variable.

Predictability

The behavior of the program is clearly defined by the type system, making it easier for developers to predict how the code will behave.

Reliability

Due to the strong validation of the type system, programs run more stably. Unexpected failures caused by type errors can be reduced.

The Importance of Soundness

Soundness plays an important role, especially when developing large-scale software projects or systems where safety is critical.

By rigorously validating the type system, errors can be found and corrected in the early stages of development, reducing maintenance costs and improving the overall quality of the software.

Soundness and Completeness

Soundness is often contrasted with completeness.

A language being complete means that its type system allows all valid behaviors of a program.

However, a language being "complete" does not necessarily mean it is sound.

Ideally, it is desirable for a type system to be sound while being sufficiently flexible to support various programming patterns.

Limitations of Soundness

Detecting all type errors at compile time can be realistically difficult or impossible.

Especially in dynamically typed languages (e.g., Ruby, Python, JavaScript), types are determined at runtime, making it difficult to catch all type errors at compile time.

Therefore, soundness is one of the goals that a programming language should pursue, but it is a property that is difficult to achieve perfectly.

When choosing or designing a programming language, soundness is an important consideration.

How strong a language's type system is, and what types of errors it can catch at compile time, directly affect the success and stability of a project.

The benefits of Soundness

• Discover Type-Related Bugs at Compile Time

  A sound type system can enforce types unambiguously.

  Therefore, type-related bugs that are hard to find at runtime can be found at compile time.

• Improves Code Readability

  Since a value has a specific type, we only need to care about the value, making the code easier to read.

  In a sound Dart language, types do not lie.

• Allows for Easily Maintainable Code

  If you change a line of code in a sound type system, the type system can warn you if it might break other parts of the code.

• Enables Good Ahead-of-Time (AOT) Compilation

  In a strong type system, AOT compilation that performs type checking in advance prevents issues like type mismatches that can occur at runtime.

  Therefore, using a strong type system with AOT compilation can improve both type safety and execution performance.

  AOT compilation refers to compiling source code into machine language or intermediate code ahead of execution. Unlike Just-In-Time (JIT) compilation, it completes compilation before running the program, leading to faster execution and advantages in initial performance optimization. Since AOT compilation runs pre-compiled machine language, it can be more efficient in memory and CPU resource usage.

• Allows Writing Cleaner JavaScript

  In web applications, limited typing operating in strong mode allows dartdevc to generate cleaner and more compact JavaScript.

Soundness and Completeness at the Static Analyzer (Code Analyzer) Level

Soundness

Guarantees that all issues identified by the analyzer are actual problems present in the code.

In sound analysis, there may be false positives (incorrect warnings), but there should be no false negatives (missed actual errors).

• False Positive

  The analyzer reports that there is an error (positive), but upon human verification, there is no error (false).

• False Negative

  The analyzer reports that there is no error (negative), but upon human verification, there is an error (false).

When trying to make the analysis more sound, the possibility of false negatives (missing actual errors) increases.

If the statements proven in the model are indeed true, the proof system is said to be "sound."

• Statements

  Properties that can be proven about the model.

• Model

  A set within a certain domain (a mathematical structure).

Completeness

Refers to the ability of the code analyzer to analyze all possible execution paths and all possible states of the program, accurately identifying the given types of errors or bugs without missing any.

When attempting more complete analysis, the complexity and execution time of the analysis increase, which can increase the number of false positives (incorrect warnings).

If the proof system can prove any true statement in the model, it is said to be "complete."

So if an analyzer judges a particular program to be "sound (accepts only true programs) and complete (rejects all false programs)," we can say that the program is 'true' and 'not false.'

This means that the Turing Machine (analyzer) halts or decides for all inputs.

Turing Machine

• A theoretical computing device first proposed by British mathematician Alan Turing.

• It consists of a tape, a head, states, and a transition function.

  1. A Turing Machine starts in an initial state.

  2. It checks the current state and the symbol it reads, then uses the transition function to determine the next action.

  3. According to the transition function, the Turing Machine moves to the next state, changes the content of the tape, and moves the head left or right.

  4. By repeating this process, the Turing Machine processes input data and performs the desired tasks.

• Turing Machine 은 이론적으로 모든 계산을 수행할 수 있는 것으로 알려져 있습니다.

Soundness and Completeness Illustrated with Examples

• Tool A (the small circle at the top left)

  • Sound and Not Complete

  • Proves that p1 and p2 have no errors

• Tool B (the circle on the left)

  • Not Sound and Not Complete

  • Proves that p3 and p4 have no errors, but fails to prove that p5 has no errors

  • p6 is located in an area that Tool B cannot verify

• Tool C (Pentagon)

  • Complete

  • Can verify all programs p1, p2, p3, p4, p5, p6

False Alarms in the Example

From the perspective of Tool A, p3 and p4 correspond to False (False Positive) Alarms

Because Tool B proved that there are no errors.

Most analyzer designers sometimes make the analyzer unsound to reduce False Negative Alarms.

Because false negatives prevent the analyzer from finding important issues from the user's perspective in some situations.

Therefore, an analyzer that only alerts to things that can be definitely called errors (True Positives) is considered a good analyzer.

From the analyzer's perspective, when all the things it reports as errors in a program are not false (False Positive Alarms), we say it is "complete."

Therefore, for a static analyzer, it is important to balance so that the analyzer is neither too sound nor too complete.

Type Safety

Luca Cardelli and Type Safety

A program being safe means that it does not cause unhandled errors (untrapped errors).

Defines a subset of all possible runtime errors as forbidden errors.

This refers to a subset of unhandled errors and handled errors (trapped errors).

A well-behaved program means that it does not produce forbidden errors.

Therefore, a well-behaved program can be said to be "safe."

A program being strongly checked means that all legal programs are well-behaved.

Strongly Checked programs have the following properties:

• Does not cause unhandled errors (Safety)

  • Does not produce unhandled errors that fall into forbidden errors

• Other handled errors may occur

Benjamin C. Pierce and Type Safety

In the context of lambda calculus, the stuck state can be formalized as follows:

If a closed term has a normal form but is not a value, we can say that the term is "stuck."

• Normal Form

  Indicates a state where the given expression can no longer be evaluated.

  Means that the expression has been evaluated to its final result and cannot be further simplified or computed.

• Closed Term

  An expression that has no free variables.

  An expression where all variables are bound within the expression, so it can be evaluated independently without depending on an external environment.

• Values

  All possible terms that can be the final result of evaluation.

• Normal Form

  When term 't' is in a state where no evaluation rules can be applied.

Through the theorem, the definition of "well-typed" is proposed as follows:

• Progress

  A well-typed term is not in a stuck state.

• Preservation

  When a well-typed term undergoes an evaluation step, the resulting term is also "well-typed."

Type Safety Introduction in easy way

Type Safety

Intuitively, the meaning of Type Safety can be described as "Well-Typed programs cannot go wrong."

This expression was coined in Robin Milner's 1978 paper 'A Theory of Type Polymorphism in Programming.'

Going Wrong

A programming language is defined by the syntax it allows developers to write and the semantics, which is the meaning of the written programs.

All programming languages face issues where a program can be syntactically correct but semantically incorrect.

The classic sentence by Chomsky, "Colorless green ideas sleep furiously," has no grammatical issues but makes no sense.

For example, in OCaml, 1 + "foo"; makes no sense when considering the semantics of the program.

Another example is in C: { char buf[4]; buf[4] = 'x'; }

This writes to index 4, which is outside the buffer's bounds, so the language definition classifies such behavior as undefined behavior (meaningless).

If we execute such meaningless programs, the program will exhibit wrong behavior.

Well-Typed

In the world of type-safe languages, the language's type system accepts only "correct" (non-wrong) programs in a certain way.

Specifically, programs accepted by the type system are called "well-typed," and type safety guarantees that such programs will never go wrong.

This can be visualized as follows:

• 

In the world of type-safe languages, well-typed programs are a subset of well-defined programs.

---

Type Safety of well known programming languages

C/C++

Not Type-Safe

The type system of C does not exclude programs that are considered meaningless according to coding standards or common developer sense (e.g., programs that go beyond the index of a buffer).

Therefore, in the C language, even well-typed programs can go wrong.

And in fact, C++, which is a superset of C, inherits these type imperfections of the C language.

Java / C#

Type-Safe

It's quite difficult to be certain that the implementation of the language is type-safe (e.g., early versions of Java's Generics had many bugs).

However, Java, as a more formalized language, can be considered type-safe.

The concept of type safety in Java gives meaning to things that were undefined in C's semantics.

For example, accessing outside the bounds of an array in a C program is undefined behavior, but in Java or C#, it is defined.

In this case, the program will throw an ArrayIndexOutOfBoundsException.

Python / Ruby

Not Type-Safe

Python and Ruby are classified as dynamically typed languages, so type-related errors can occur at runtime.

They throw exceptions at runtime for type errors to signal type errors.

Therefore, these programs are well-defined according to the language's semantics.

In Java, if a program o.m() is well-typed, type safety guarantees that o is an object that has a method m that takes no arguments, and the method call will succeed.

In Ruby, executing a program o.m() that is well-typed according to Ruby's type system cannot guarantee that o defines the method m; the call may succeed or an exception may occur.

Type safety does not simply mean one thing. What it guarantees depends on the language's semantics and may involve incorrect behavior.

In Java, calling a non-existent method is incorrect behavior (it will fail to compile).

In Ruby, calling a non-existent method is not incorrect behavior (it will simply raise an exception).

Javascript

Not Type-Safe

Because it uses a dynamic type system.

It's difficult to catch type-related errors at compile time, which increases the likelihood of type errors occurring at runtime.

Using TypeScript allows for type-safe usage (by adding a static type system).

Go

Generally Type-Safe

Classified as a statically typed language; the compiler checks the types of variables and expressions to prevent type-related errors in advance.

However, it does not enforce explicit type annotations; it uses type inference.

In summary, it emphasizes type safety and tries to ensure stability through static type checking.

Kotlin

Type-Safe

Strictly checks the types of variables and expressions at compile time.

Emphasizes null safety, explicitly specifying whether a variable can hold a null value.

Ensures stability through static type checking.

Scala

Strongly Type-Safe

Strictly checks the types of variables and expressions at compile time.

The type system is powerful, providing high levels of abstraction and flexibility while ensuring safety from type errors.

The type inference feature improves code readability and conciseness while ensuring type correctness.

Rust

Strongly Type-Safe

Checks all types at compile time.

Uses a strong type system and ownership model to guarantee memory safety at compile time.

Prevents many types of bugs and unsafe behaviors that can occur at runtime.

The type system works by explicitly declaring the types of variables, functions, expressions, etc., or by letting the compiler infer the types.

The ownership system prevents concurrency errors like data races at compile time.

It prevents variables from having multiple owners and allows only one modification of data at a time, enabling safe concurrent programming.

Benefits of Type-Safe Programming Language

Error Reduction

• Type-safe languages force detection and correction of type-related errors at compile time.

• This greatly reduces errors that can occur at runtime, helping to create more stable programs.

Facilitates Code Maintenance

• A type system clarifies the intent of the code and helps other developers understand and modify the code.

• Type declarations and checks serve as code documentation, and the benefits become more pronounced as the codebase grows larger and more complex.

Increased Safety in Refactoring

• Type checking allows for early detection of errors that may occur during refactoring.

• Type safety acts as a safety net that prevents code changes from causing unexpected side effects.

Improved Automated Tool Support

• Type information is utilized by tools like IDEs (Integrated Development Environments) to provide various features such as code auto-completion, static analysis, and refactoring support.

• This greatly enhances developer productivity.

Possibility of Performance Optimization

• Compilers can perform optimizations using type information.

• For example, optimizations like memory layout optimization based on data types or reducing type checks at runtime.

Increased Security

• Type safety can help prevent certain types of security vulnerabilities.

• For example, memory-related errors like buffer overflows can be effectively managed through the type system.

---

White House Urges Developers to Dump C and C++

The White House guides developers to abandon C and C++ and use safe programming languages like Rust.

US President Joe Biden’s administration wants software developers to use memory-safe programming languages and ditch vulnerable ones like C and C++.

Memory-safe programming languages are protected from software bugs and vulnerabilities related to memory access, including buffer overflows, out-of-bounds reads, and memory leaks.

The new 19-page report from ONCD gave C and C++ as two examples of programming languages with memory safety vulnerabilities, and it named Rust as an example of a programming language it considers safe.

---

Linus Torvalds: Rust Will Go into Linux 6.1

Linus Torvalds says that code written in Rust will be included in Linux 6.1.

---

Summary

Sound programs have many advantages, and this is greatly influenced by how the type system is designed.

Ultimately, type safety and soundness are closely related, and programming language designers need to balance them well.

The reason why type-safe programming languages are gaining attention today is that type systems like those in C and C++ allow memory-related errors that cause security issues by permitting programs that are syntactically correct but semantically incorrect to some extent.

Type-safe programming languages have many advantages in terms of productivity and stability, so it's good to use these features appropriately where applicable.

References

• Type Safety in OCaml Language (Youtube)

• What is soundness in static analysis?

• False Positives in Static Code Analysis

• Type Systems for Programming Languages

• The Type System Every Programmer Should Know

• A Type System From Scratch – Robert Widmann (Youtube)

• Types and Programming Languages (Book)