Designing a new Language for Safety: Fuzion
A minimal language for safety-critical systems
<p>Fuzion is a modern general purpose programming language that unifies concepts
found in structured, functional and object-oriented programming languages into
the concept of a Fuzion feature. It combines a powerful syntax and safety
features based on the design-by-contract principle with a simple intermediate
representation that enables powerful optimizing compilers and static analysis
tools to verify correctness aspects.</p>
<p>This talk will focus on Fuzion's aspects related to safety-critical software
development. A fundamental idea of Fuzion is to provide a simple language at a
high level of abstraction and move implementation decisions from the developer
to the compiler. To enable this, the language defines a simple but powerful
intermediate representation for static analysis tools to operate on.</p>
<p>Furthermore, pre- and post-conditions for design-by-contract are provided in a
way that enables different levels of verification: static analysis as well as
dynamic checks at different levels from safety to debugging.</p>
<p>Fuzion does not support exceptions, a run-time error has to be part of the result
of a call and must be checked explicitly. Fuzion does not support dynamic
loading of code. Numeric operations such as 'infix +' check for overflow.</p>
<p>Fuzion applications consist of a set of library modules and a main modules.
Modules are verified for correctness individually as well as whole
applications. This is possible since dynamic loading of code is not supported.</p>
Introduction
Fuzion is a modern general purpose programming language that unifies concepts
found in structured, functional and object-oriented programming languages into
the concept of a Fuzion feature. It combines a powerful syntax and safety
features based on the design-by-contract principle with a simple intermediate
representation that enables powerful optimizing compilers and static analysis
tools to verify correctness aspects.
Fuzion was influenced by many other languages including Java, Python, Eiffel,
Rust, Go, Lua, Kotlin, C#, F#, Nim, Julia, Clojure, C/C++, and many more. The
goal of Fuzion is to define a language that has the expressive power present in
these languages and allow high-performance implementations and powerful analysis
tools. Furthermore, Fuzion addresses requirements for safety-critical
applications by adding support for contracts that enable formal specification and
enable detailed control over run-time checks.
Many current programming language are getting more and more overloaded with new
concepts and syntax to solve particular development or performance issues.
Languages like Java/C# provide classes, interfaces, methods, packages, anonymous
inner classes, local variables, fields, closures, etc. And these languages are
currently further extended by the introductions of records/structs, value types,
etc. The possibility of nesting these different concepts results in
complexity for the developer and the tools (compilers, VMs) that process and
execute the code.
For example, the possibility to access a local variable as part of the closure
of a lambda expression may result in the compiler allocating heap space to hold
the contents of that local variable. Hence, the developer has lost control over
the allocation decisions made by the compiler.
In Fuzion, the concepts of classes, interfaces, methods, packages, fields and
local variables are unified in the concept of a Fuzion feature. The decision
where to allocate the memory associated with a feature (on the heap, the stack
or in a register) is left to the compiler just as well as the decision if
dynamic type information is needed. The developer is left with the single
concept of a feature, the language implementation takes care of all the rest.
Fuzion Feature Declarations
A Fuzion feature has a name, similar to the name of a class or a function.
The main operation that can be performed on a feature is a feature call. The
constituents of a feature declaration are as follows:
Formal Arguments
Features may have a list of formal arguments, which are themselves features
implemented as fields. On a call to a feature with formal arguments, actual
arguments have to be provided to the call, unless the list of formal arguments
is empty.
Feature Result
The result of a feature call is an instance of the feature. Alternatively, a
feature may declare a different result type, then it must return a value of that
type on a call.
Closures
Features are nested, i.e., every feature is declared within the context of an
outer feature. The only exception is the universe, which is the outermost
feature in Fuzion. A feature can access features declared in its
outer feature or, recursively, any outer feature of these outer features. This
means, a feature declaration also defines a closure of the feature and its
context.
When calling a feature f1 declared as an inner feature of f2, the call must
include a target value which is the result of a call to f2, e.g., f2.f1.
Generics
Features may have generic type parameters. E.g. a feature declaration may leave
the actual type used within that feature open and to be defined by the user of
the feature.
The list of generic type parameters may be open, i.e., the number of actual
generic type parameters is not fixed at feature declaration. This turns out to
be useful in the declaration of choice types and functions as explained below.
Inheritance
Fuzion features can inherit from one or several other features. When inheriting
from an existing features, all inner features of the parent automatically become
inner features of the heir feature. It is possible to redefine inherited
features. In particular, when inheriting from a feature with abstract inner
features, one can implement the inherited abstract features.
A redefinition of an inherited feature may implement an inherited feature as a
routine or as a field. An inherited feature that is implemented as a field,
however, cannot be redefined as something else since fields might be mutable.
Inheritance may result in conflicts. An example would be two features with the
same name that are inherited from two different parents. In this case, the heir
must resolve the conflict either by redefining the inherited features and
providing a new implementation or by renaming the inherited features resulting
in two inner features in the heir feature.
Inheritance and redefinition in Fuzion does not require dynamic binding. By
default, the types defined by features are value types and no run-time overhead
for dynamic binding is imposed by inheritance.
A Contract
A feature may declare a contract that specifies what the features does and under
which conditions the feature may be called.
An implementation
Features must have one of the following implementations
a routine is a feature implementation with code that is executed on a call
a field is a memory slot that stores a value and whose contents are returned on a call
an abstract feature has no implementation and cannot be called directly, but can be implemented by heir features
an intrinsic feature is a low-level feature implemented by the compiler or
run-time system, e.g., the infix + operator to add two 32-bit integer values
may be an intrinsic operation.
A feature implemented as a routine can contain inner feature declarations.
Feature examples
Here is an example that declares a feature point that functions similar to a
struct or record in other languages:
point(x, y i32) is # empty
p1 := point 3 4
say "p1.x is {p1.x}" # will print "p1.x is 3"
say "p1.y is {p1.y}" # will print "p1.y is 4"
The next example shows a feature base that provides an inner feature plus
that adds its argument to the value passed to the enclosing base:
base(v i32) is
plus(w i32) => v + w
b1 := base 30
b2 := base 100
say (b1.plus 23) # will print "53"
say (b2.plus 23) # will print "123"
Design-by-Contract
Fuzion features can be equipped with pre- and post-conditions to formally
document the requirements that must be met when a feature is called and the
guarantees given by a feature. An example is a feature that implements a square
root function for 32-bit integers:
sqrt(a i32) i32
pre
safety: a >= 0
post
debug: result * result <= a,
debug: (result + 1) > a / (result + 1),
debug: result >= 0
is
if a == 0
0
else
for
last := 0, r
r := 1, (last +^ a / last) / 2 # +^ performs saturating addition
until r == last
In this case, the function defines the pre-condition that its argument
'a' is non-negative. A call of this function with a negative value will
result in a run-time error. On the other hand, its post-conditions make a clear
statement about the result: The result will be the largest value that, when
squared, is less than or equal to 'a'.
Checking Pre- and Post-conditions
Pre- and post-conditions can be classified for different purposes. Default
qualifiers provided in the standard library are
safety
This qualifier protects pre-conditions that are required for the safety of an operation.
An example is the index check pre-condition of the intrinsic operation to
access an element of an array: Not performing the index check would allow
arbitrary memory accesses and break the application's safety.
This qualifier should therefore never be disabled unless you are running code
in an environment where performance is essential and safety is irrelevant.
debug, debug(n)
This qualifier is generally for debugging, it is set iff debugging is
enabled or enabled at the given level, respectively..
pedantic
This qualifier is for conditions that a pedantic purist would require, that
otherwise a more relaxed hacker would prefer to do without.
analysis
Qualifier for conditions that are generally not reasonable as
run-time checks, either because they are prohibitively expensive or even not
at all computable in this finite universe. These conditions may, however, be
useful for formal analysis tools that do not execute the code but
perform techniques such as abstract interpretation or formal deduction to
reason about the it.
Additional user defined qualifiers may be added, any expression resulting in a
'bool' can be used.
Run-time checks for pre- and post-conditions can be enabled or disabled for each
of these qualifiers (except for 'analysis', which is always disabled). This
gives a fine-grain control over the kind of checks that are desired at run-time.
Usually, one would always want to keep safety checks enabled in a system that
processes data provided from the outside to avoid vulnerabilities such as buffer
overflows. However, in a closed system like a rocket controller, it might make
sense to disable checks since a run-time error would mean definite loss of the
mission, while an unexpected intermediate value may still result in a useful
final result of a calculation.
Explicit results instead of Exceptions
Instead of exceptions that provide an alternative path for a function to return,
Fuzion requires all functions to return a result. To indicate failure, the
generic result type 'outcome' is provided.
outcome is a choice type that represents the result of a routine that
may either produce something useful or fail producing an error condition.
Here is a small example of using an outcome result
getData (u User, t Type) outcome<data> is
if u.allowedToAcces T
(readFile t.fileName)?
else
error "user $u not allowed to access $t"
readFile (n string) outcome<data> is
if dataExists n
readData n
else
error "data $t not available"
A user of this code when would have to explicitly unwrap the read data as follows
o := getData user type
match o
d data => say "success: $d"
e error => say "*** error $e"
Fuzion Modules
Modules in Fuzion are collections of Fuzion features that form a library to be
used by other modules. Modules may define a main entry point, such that they can
be used to build applications.
The Fuzion front end performs static code analysis at the module level. This
means that any features exported by a module are save to be used in different
contexts by other modules. This includes static checking of the following
aspects:
Field Initialization
In Fuzion, the front end ensures that all fields are assigned an initial value.
There is no default initial value for uninitialized fields and there is no means
to access an uninitialized fields, as there is, e.g., for final fields in Java.
Instead, it is checked that whenever an instance containing a field becomes
accessible outside of the feature declaring that field, the call chain is
analyzed to ensure it may not contain any accesses to the field. In particular,
if an instance may become visible outside of the module, no uninitialized field
may be accessible by any exported features of that module.
Function Purity
The result of any feature visible to the outside must be independent of state
modifiable by other exported features and must not itself modify state that may
affect the result of other exported features. This purity will allow
optimizations such as memoization or lazy evaluation common in functional
languages.
Nevertheless, a pure function may use mutable fields, e.g., to store
intermediate results during its calculations. If the mutable field's life span
is limited to the call of the exported feature and the field is not accessed by
any other exported feature, mutation does not make a function impure.
Race Freedom
Closely related to function purity is race freedom: Any exported feature is
checked to be safe to be called in a threaded environment without causing data
races. There are no explicit locks in Fuzion, so there is no danger
of deadlocks due to nested locking.
Immutability
Fuzion encourages the use of immutable data by simple syntax for the declaration
of immutable fields. Also, the use of tail calls for loops automatically
converts iterator variables used in that loop into immutable variables with a
life span of a single loop iteration.
Since immutability is essential to ensure correctness of parallel execution
within threads that do not rely on locks or similar synchronization mechanisms,
Fuzion's analyzer will verify that data shared between threads is immutable.
The standard library has been designed to provide immutable data types.
Nevertheless, there are mutable types such as 'marray', which provides a
mutable array. These, however, should be used for local calculations only,
escape analysis will ensure that no accesses to mutable types occur from
outside the code manipulating the state.
Memory Management
Fuzion to a large extend relies on static analysis to reduce memory management
overhead. Instances are by default value instances that do not require heap
allocation. Furthermore, immutability in many cases avoids the need to keep a
shared copy on the heap. For dynamic calls, heap allocation and dynamic binding
overhead is avoided by specialization of calls.
Only for those instances for which all of these optimizations would fail, in
particular instances shared between threads or long-lived instances with mutable
fields, heap allocation will be required. Memory allocated on the heap will be
reclaimed by a real-time garbage collector.
Fuzion Thread Safety
Static analysis at module and application level ensure that mutable data is not
shared between threads in Fuzion. However, there must be means for threads to
communicate, e.g., for the result of a thread to become available to other
threads. How this will be done in Fuzion is still open, thread safe libraries
such as thread-safe queues between might be provided here.
Conclusion and Next Steps
I hope Fuzion shows some interesting ideas how to approach the development of
safety-critical software.
The Fuzion language definition and implementation are far from stable, but are
getting closer to become useful. Currently, two execution options for Fuzion
are available: An interpreter implemented in Java and a back-end that compiles to
C code. A tool to interface Java code is available for the interpreter.
Main points that are missing right now are
a powerful standard library
additional library modules for all sorts of application needs
low-level foreign language interface for C
actual implementations of static analyzers and optimizers
highly optimizing back-ends
garbage collection for the C back-end
documentation, tutorials
enthusiastic contributors and users!
Please feel free to contact me in case you want to use Fuzion or want to help
making it a success!
Additional information