Define the MVP semantic core

Define the MVP semantic core

Type: grilling Status: resolved Parent: Find the ASPL MVP specification

Question

What exact static types, expressions, variable and mutability rules, function semantics, control flow, string-literal behavior, source-file structure, and explicitly unsafe operations belong to the tiny MVP language core, and which acceptance programs prove that this core is internally coherent?

Answer

The MVP semantic core is a small, statically typed language with checked integer arithmetic, deterministic evaluation, immutable-by-default lexical bindings, typed top-level functions, literal-only strings, and an operation-local unsafe boundary for C calls. This ticket fixes behavior, not source spelling, VM representation, or the C adapter catalog.

Types and checking

• Storable values have exactly five types: bool, i64, f64, immutable UTF-8 string, and opaque nullable c_ptr.
• unit is a result type, not a storable value. A unit function may end naturally or use a bare return. A call returning unit is valid only as a statement. Programs cannot create, store, pass, or compare unit values.
• Exact C ABI types exist only in foreign declarations. The dynamic C interoperability decision must define their explicit boundary conversions without adding implicit conversions to ordinary ASPL code.
• Types never convert implicitly. Local inference selects the initializer's exact type. An explicit annotation must match after any written conversion, and a mutable local keeps one type for its lifetime.

Programs and names

• A program is one source file containing ASPL function definitions and foreign declarations. File scope permits no variables or executable statements.
• Exactly one defined ASPL function is named ابدأ_الرئيسية or start_main. It takes no parameters, returns i64, cannot be foreign, and cannot be called by ASPL source.
• An entry-function result from 0 through 255 becomes the process status. Any other result traps instead of being truncated.
• ASPL functions, foreign declarations, and the release-fixed builtin catalog share one top-level callable namespace. Duplicate names and overloads are errors, and source cannot replace a builtin alias.
• A local or parameter cannot reuse any currently visible local, parameter, ASPL function, foreign name, or builtin alias. A local name may be reused after its previous scope ends.

Bindings and scopes

• Function bodies and nested control-flow blocks introduce lexical scopes.
• Every local has an initializer. The declared name becomes visible only after the checker has checked that initializer.
• Bindings and parameters are immutable by default. A local declaration may explicitly opt into mutation; parameters cannot.
• Assignment is a statement that targets one mutable local. It evaluates the entire right side before changing the target and produces no value.
• The MVP has no globals and no shadowing of a visible name.

Functions

• Functions appear only at file scope and require parameter and result types. There are no nested functions, closures, methods, default arguments, variadic ASPL functions, or function values.
• Source order does not affect resolution. Direct recursion, mutual recursion, and calls to later definitions are valid.
• ASPL and builtin calls pass arguments by value, require exact arity, and require exact argument types after explicit conversions. Foreign calls use their separately specified boundary conversions.
• Every reachable path through a non-unit function must return a value of its declared type. A structural if proves a return only when both branches return. A while never proves a containing function returns, even when its condition is a literal true value.
• The checker rejects code that the same structural analysis proves unreachable. It does not use constant folding or theorem proving for reachability.

Expressions and statements

• Expressions are literals, local or parameter references, ASPL calls, safe builtin calls, explicitly unsafe foreign calls, explicit numeric conversions, grouping, and the specified unary and binary operations.
• Functions are not values. Assignment, conditionals, increments, decrements, and implicit calls are not expressions. There is no general cast expression beyond the specified conversions and later explicit C boundary conversions.
• Statements are initialized local declarations, assignment, calls, if, while, and return.
• A non-unit call may be used as a statement and discard its result. No other value-producing expression may stand alone as a statement.

Numeric behavior

• Integer literals have type i64; floating literals have type f64. An out-of-range literal is a checking error.
• The source form -9223372036854775808 is accepted as the minimum i64 value even though its magnitude does not fit as a positive i64 literal. Negating that value at runtime traps.
• i64 supports unary negation, +, -, *, /, %, equality, and ordered comparisons. Integer overflow traps.
• Signed division truncates toward zero. Remainder has the dividend's sign or is zero, and satisfies a matches (a / b) * b + (a % b).
• Integer division and remainder trap for a zero divisor and for i64 minimum with -1.
• f64 supports unary negation, +, -, *, /, equality, and ordered comparisons. It follows IEEE 754 binary64 behavior, including infinities, signed zero, and NaN.
• Explicit i64 to f64 conversion uses IEEE 754 rounding. Explicit f64 to i64 conversion truncates toward zero and traps for NaN, infinity, or an out-of-range result.
• Bitwise operations and shifts are not in the MVP.

Booleans and equality

• Only bool is valid as an if or while condition. There are no truthiness conversions.
• Boolean and and or short-circuit. Boolean not is unary.
• Equality requires operands of the same type. Booleans and integers compare by value, floating equality follows IEEE 754 behavior, strings compare exact UTF-8 contents, and pointers compare identity including null. unit has no equality operation.

Strings

• A string is an immutable UTF-8 value created only from a literal. String contents receive no runtime normalization.
• Strings may be stored, passed, returned, discarded, and compared. They may contain an embedded NUL.
• The core has no concatenation, indexing, slicing, interpolation, mutation, or runtime string construction. C-string conversion and lifetime rules belong to dynamic C interoperability.

Pointers and unsafe operations

• c_ptr has a null literal. Ordinary code may store, pass, return, discard, and compare a pointer.
• Ordinary code cannot dereference a pointer, perform pointer arithmetic, inspect its address, or convert between pointers and integers or strings.
• Only an unsafe foreign call may introduce a non-null pointer from outside ASPL or send one back across the foreign boundary. ASPL functions may relay the opaque value without inspecting it.
• Every foreign declaration and every foreign call is explicitly unsafe at its own use site. The MVP has no general unsafe block.

Control flow, evaluation, and traps

• if with an optional else and while are statements with lexical block bodies. break and continue are not in the MVP.
• return is the only early-exit statement.
• Operands, call arguments, and initializers evaluate left to right. Assignment evaluates its complete right side before changing the target. Boolean short-circuiting preserves this order.
• A runtime trap immediately and uncatchably terminates the whole ASPL program. Nothing after the failing operation runs. Later diagnostics and CLI decisions must assign messages and exit codes without changing which operations trap.

Acceptance programs

The notation decision must render these as equivalent Arabic-keyword and English-keyword source fixtures. Each rejection and trap is a separate program so an earlier failure cannot hide another.

Programs that succeed:

• sum_loop uses a mutable local and while to sum 1 through 10, then returns 55.
• recursive_factorial computes factorial of 5 and returns 120.
• mutual_recursion defines even and odd checks in reverse dependency order and proves that mutual recursion resolves independently of source order.
• short_circuit places integer division by zero in Boolean branches that must not execute.
• string_identity passes and returns an Arabic string containing an embedded NUL, then compares it with the original.
• float_round_trip explicitly converts 42 from i64 to f64 and back.
• unit_call calls a unit helper as a statement.
• builtin_output calls the safe (string) -> unit output builtin as a statement and writes the exact literal bytes without an added newline.
• null_round_trip passes null through a c_ptr identity function and compares the result with null.
• maximum_status returns process status 255 successfully.

Programs rejected during checking cover each of these independently:

• Wrong-type arithmetic, comparison, condition, assignment, return, argument, or equality operands.
• An attempted implicit conversion or an out-of-range numeric literal.
• A local without an initializer, assignment to an immutable binding, or assignment of a different type.
• Shadowing of a local, parameter, ASPL function, foreign declaration, or builtin alias.
• A global binding or executable top-level statement.
• A duplicate or overloaded callable, missing or invalid entry function, or source call to the entry function.
• Wrong call arity, a missing return path, or structurally unreachable code.
• Any attempt to create, store, pass, or compare unit.
• Pointer arithmetic, dereference, address inspection, or pointer conversion.
• An unmarked foreign declaration or foreign call.
• Any excluded expression or statement form.

Programs that trap at runtime cover each of these independently:

• Checked integer overflow, including negation of i64 minimum.
• Integer division or remainder by zero.
• i64 minimum divided or remaindered by -1.
• NaN, infinity, and out-of-range f64 to i64 conversions.
• The entry function returning below 0 or above 255.

The runtime value model must preserve these semantics in bytecode execution. Dynamic C interoperability must add a concrete foreign-call fixture. Diagnostics, CLI, playground, and final conformance decisions must preserve the same checking and trap outcomes in every environment where the relevant operation is supported.