41–50 of 144 posts
> 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.
Both of these checks happen at runtime in Rust. Overflow checks in particular only happen in debug mode, not in release mode.
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…
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…
> Wuffs looks really interesting! I don't think I've ever even heard of a language that is designed to only be used in an auxiliary role along side another general purpose programming language! 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.
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…
> A type that depends on another value. For example, a variable n’s type might be “the length of s”, for some other slice-typed variable s. 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.
Earlier quoted context omitted.
> Wuffs looks really interesting! I don't think I've ever even heard of a language that is designed to only be used in an auxiliary role along side another general purpose programming language! 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.
It compiles to C.
Another tool along these lines is Galois' Ivory language https://ivorylang.org/ , a Haskell-embedded language for writing safe/reliable C.
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…
All of Windows (including the NT kernel) is written using the same basic proof model that Wuffs uses, except that the constraints are specified as annotations on top of C and C++ instead of as a new programming language. 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…
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…
All of Windows (including the NT kernel) is written using the same basic proof model that Wuffs uses, except that the constraints are specified as annotations on top of C and C++ instead of as a new programming language. 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…
Another tool along these lines is Galois' Ivory language https://ivorylang.org/ , a Haskell-embedded language for writing safe/reliable C.