The site sections are under development.

The materials may be incomplete or contain errors. The site content will be synchronized with the implementation in the next release, while the current version (0.6.0) is intended for syntax prototyping and for creating the playground.

Guarantees and safety

Overview of TrustLang features responsible for code safety and quality
Tags:

This section brings together the TrustLang capabilities that are responsible for the safety and quality of programs: safe memory management, protection from data races, correctness control at compile time and formal verification.

Each capability is described in detail in exactly one place (the source page) and is only mentioned here with a summary and a link. Detailed lists of options/diagnostics are not duplicated — their source is the tool’s help (trust --help, trust -Whelp, LSP hovers).

Capabilities of the section

Capability Briefly In detail (source)
Safe memory management without GC RAII, strong/weak references, prohibition of strong cyclic references, protection from stack overflow Memory
Protection from races and access synchronization Automatic inter-thread synchronization when accessing shared data Memory
Contract programming Pre/postconditions and assertions (trust_pre/trust_post/trust_assert) Verification
Formal verification (SMT) Automatic execution of Z3 over contracts, loop invariants, quantifiers Verification
Static typing and conversion control Nominal type checking at compile time; narrowing with range control Type system
Range checks of numbers An error when leaving the type range, instead of silent overflow Numbers
Integer overflow control Built in and enabled by default: overflow of signed arithmetic (UB in C++) → catchable IntMinus Numbers
Stack overflow protection (stack check) Stack overflow → catchable stack_overflow exception, not a segfault stack_check
Control of reference invalidation (borrowed) Prohibition of using dependent references after mutation of the source (dangling references) invalidation

The safe memory model has been ported to C++ in a separate project memsafe.

  • Multithreading and asynchrony (coroutines, :AsyncTask/:AsyncPool) is a functional language capability, not a safety feature; it is described in Expressions and control flow. Only the race protection provided by the reference model from Memory is related to safety.
  • Implementation status — the boundaries of the implementation of the features of this section.
Memory management and shared access

Stack overflow protection (stack check)

Turning a stack overflow into a catchable exception instead of abnormal termination