31–40 of 144 posts
I would be interested how much their approach scales in terms of code size, since they use likely SMT solvers to guarantee having no arithmetic overflows (which is more than Rust guarantees). Ideally as comparison with compile times of Rust programs.
Earlier quoted context omitted.
Looks like there isn't an encoder for PNG: https://github.com/google/wuffs/tree/main/std/png Given the project goals, I guess most encoders don't make a lot of sense: For image encoding you basically provide an "x * y * bytes_per_pixel" memory area and an encoder does its magic on that. There isn't really any complicated untrusted input in that case.
The performance tradeoff isn't as justifiable, either: most images are decompressed orders of magnitude more times than they're compressed (generally just once).
However it isn’t obvious whether such companies have any incentive to share their code, even just because the code is too specific to their hardware?
Interesting. First time I've head of Wuffs. As someone that still uses C, this in particular sounds neat: (from https://github.com/google/wuffs#goals-and-non-goals ) """ Wuffs' goal is to produce software libraries that are as safe as Go or Rust, roughly speaking, but as fast as C, and that can be used anywhere C libraries are used. [...] Wuffs the Library is available as transpiled C code. Other C/C++ projects can u…
It seems like this would be an interesting approach to a lot of security programming where it involves data structures, since those have typically been a source of issues. Having a memory-safe ASN.1 parser would be really nice, considering how much difficulty that has caused in the security space.
With a lot of security programming there's a reliance on constant-time algorithms, which this may not be well-suited to, however.
> Also, unlike Go or Rust, Wuffs’ memory safety is enforced at compile time, not by inserting runtime checks that e.g. the i in a[i] is within bounds or that (x + y) doesn’t overflow a u32. Am I missing something, or is this statement simply wrong? Have not used Go, but Rust checks its stuff at compile time as far as I know.
Are there any compiletime benchmarks? I would be interested how much their approach scales in terms of code size, since they use likely SMT solvers to guarantee having no arithmetic overflows (which is more than Rust guarantees). Ideally as comparison with compile times of Rust programs.
At least based on a quick skim of the docs, they use a combination of programmer assertions, interval arithmetic, and their type system for bounds checking and ensuring no arithmetic overflows.
> Also, unlike Go or Rust, Wuffs’ memory safety is enforced at compile time, not by inserting runtime checks that e.g. the i in a[i] is within bounds or that (x + y) doesn’t overflow a u32. Am I missing something, or is this statement simply wrong? Have not used Go, but Rust checks its stuff at compile time as far as I know.
let a = [0;4];
println!("{}", a[5]);
let a = 128u8 + 128u8;
Interesting. First time I've head of Wuffs. As someone that still uses C, this in particular sounds neat: (from https://github.com/google/wuffs#goals-and-non-goals ) """ Wuffs' goal is to produce software libraries that are as safe as Go or Rust, roughly speaking, but as fast as C, and that can be used anywhere C libraries are used. [...] Wuffs the Library is available as transpiled C code. Other C/C++ projects can u…
I prefer the annotation approach, TBH, but I'm glad to see people working on safety. Specifically, Wuffs (like Rust) has this problem where it tries to fill the same niche as C and C++ and improve on these older languages in specific ways, but in addition to being different in ways necessary to achieve the language's objective is also different from C and C++ in totally gratuitous ways that are basically just aesthetic differences --- for example, "type var" vs "var: type".
I'm a big believer in technical continuity. IMHO, a lot of recent language developments should have instead been extensions of C, C++, Java, or Python.
My favorite part of the Wuffs github page has to be the definition it gives for Dependent Types > ...Dependent types are a way to implement compile-time bounds checking, but they're not the only way, and there's more to programming languages than their type systems. Wuffs does not use dependent types. Wuffs looks really interesting! I don't think I've ever even heard of a language that is designed to only be used in…
It's positioned somewhat separately as you don't codegen from it, but TLA+? It exists to model and verify a program, but you still write the program separately.
Are there any compiletime benchmarks? I would be interested how much their approach scales in terms of code size, since they use likely SMT solvers to guarantee having no arithmetic overflows (which is more than Rust guarantees). Ideally as comparison with compile times of Rust programs.
> since they use likely SMT solvers to guarantee having no arithmetic overflows At least based on a quick skim of the docs, they use a combination of programmer assertions, interval arithmetic, and their type system for bounds checking and ensuring no arithmetic overflows.
Also loop invariants etc must all be annotated. I would be more interested how they plan to handle IO effects or if they want to omit that.