f32 is a type of the language: literals typed by use, no mixing with f64, f64 as f32 aborts beyond range (ADR-285 D33)Open and answer this issue on GitHub.
language, compiler, ready · opened 2026-10-08 · updated 2026-10-10 · 1 comment
#470 asked whether a written usize, i16 or f32 is refused, since Part I 2.2 offers only i64, i32, u8, u64, u32 and f64. In the decision round (2026-10-08) the owner answered (a) for the others: usize, isize, i8, i16, u16, i128, u128 and str are refused with NK1135. For f32 the owner’s call was that it is clearly part of the language.
The reasons are in ADR-285 D33:
f32 is a float type beside f64.f64 unless its use asks for an f32: let w: f32 = 0.5.f32 and an f64 do not mix without as.f32 as f64 always fits.f64 as f32 rounds to the nearest f32. A finite value beyond the f32 range aborts, as an integer that does not fit does; an infinity and NaN carry over.The rules are taken from the ones already set for numbers (ADR-285), so f32 adds no rule of its own. The abort on f64 as f32 is the one derived choice: it follows D1 (a value that does not fit stops the program), where Rust saturates to infinity.
fn take(x: f32) -> f32 { return x } passes the checker, because types.nika’s BUILT_IN lists every Rust primitive. Arithmetic with a literal, or with an f64, then fails in rustc.
f32 is a number type everywhere f64 is (integer_named’s float counterpart, NK1122’s list and its note “The number types are …”). A float literal takes f32 from its use, as an open integer does (ADR-285 D23). Mixing f32 and f64 without as is refused like two integer types.
Tests: let w: f32 = 0.5; fn half(x: f32) -> f32 { return x * 0.5 }; x + y with x: f32, y: f64 refused, naming as.f64 as f32 emits a checked narrowing that aborts on a finite value beyond f32::MAX. Tests: 1e39 as f32 aborts at run time; (1.0 / 0.0) as f32 is infinity; 0.1 as f32 rounds.std: the float methods f64 has in std.contracts (sqrt, abs, floor, the truncating_* conversions, formatting in f"…") get f32 entries, written by hand as D36 says. Test: each called on an f32.f32 values prints them as Rust’s f32 Display does.f32 goes in with step 1, and BUILT_IN loses the types #470 refuses in the same change.
f64 as f32 does not abort; it is shown to fit, or the program says what it wants0.0.701 had f64 as f32 abort on a finite value beyond the f32 range. The owner’s rule (0.0.702, ADR-285 D33, Part I 2.2, Part III C.3):
NK1116, as for integers (D29).as f32 the compiler does not show to fit is NK1241. The help names the two ways to write it:
x.checked_f32() gives an f32?, which is null beyond the range;x.rounding_f32() is Rust’s behaviour: the nearest f32, and infinity beyond the range.What that means today. The prover reasons about integers and not about floats (ADR-270 D11). Until it does, every non-constant f64 as f32 is NK1241. D1’s integer as (an abort) is not changed by this.
f32 is a number type everywhere f64 is (NK1122’s list and its note). A float literal takes f32 from its use (ADR-285 D23). Mixing f32 and f64 without as is refused like two integer types.
Tests: let w: f32 = 0.5; fn half(x: f32) -> f32 { return x * 0.5 }; x + y with x: f32, y: f64 refused, naming as.f64 as f32:
f32::MAX is NK1116;(a as f64) as f32 with a: f32, converts;as f32 is NK1241, with both names in the help.Tests: 1e39 as f32 is NK1116; 0.5 as f32 converts; x as f32 with x: f64 a parameter is NK1241.
checked_f32 and rounding_f32 on f64, as std.contracts entries (written by hand, D36) with their lowering.
Tests: 1e39.checked_f32() is null; 1e39.rounding_f32() is infinity; 0.1.checked_f32() is the nearest f32; NaN carries over in all three forms.std: the float methods f64 has (sqrt, abs, floor, the truncating_* conversions, formatting in f"…") get f32 entries. Test: each called on an f32.f32 values print as Rust’s f32 Display does.Generated by Claude Code