Earlier quoted context omitted.
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…
What tool/framework do they use for annotation and are there standards like SMTlib2, but for annotating those kind of things? Can this tools verify that the annotations are correct wrt the code below or above?
Wuffs’ PNG image decoder
51–60 of 144 posts
Re: Wuffs’ PNG image decoder
#52Surprisingly, Go's png decoder is half as slow as the default libpng :(
https://nigeltao.github.io/blog/2021/fastest-safest-png-deco...
Re: Wuffs’ PNG image decoder
#53Earlier 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).
I’m not sure I would take that bet. How much security camera footage is compressed, recorded, never looked at, and discarded after x days?
Certainly in number of images (as opposed to number of bytes), those might tilt things the other way.
Re: Wuffs’ PNG image decoder
#54Earlier quoted context omitted.
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…
But the C++ spec has become quite unwieldy, so I can understand the desire to start a totally new language.
The previous post on the blog has an observation that applies to languages as well
> Software has a Peter Principle. If a piece of code is comprehensible, someone will extend it, so they can apply it to their own problem. If it’s incomprehensible, they’ll write their own code instead. Code tends to be extended to its level of incomprehensibility.
Re: Wuffs’ PNG image decoder
#55Interesting. 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…
I work on (well, mostly near) an extensible C compiler, designed so extension authors can independently create extensions, and users can import them as easily as libraries: https://github.com/melt-umn/ableC/ (and I'd love to answer any questions you have about our approach or code.)
IMO this approach hasn't taken off because maintaining compatibility with C while adding safety (or really just about any property) means implementing your own sublanguage that can't arbitrarily call C functions while maintaining your safety properties. On the other hand, C being able to call into your sublanguage easier is a benefit versus jury-rigging Cargo into your build system (in the case of Rust).
On the other hand, this approach works great for adding extensions that increase the expressive power of C with new abstractions, for example algebraic data types, C++-like templating, etc.
Re: Wuffs’ PNG image decoder
#56So will it makes its way into browsers?
Re: Wuffs’ PNG image decoder
#57My 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…
Wasm does at runtime what Wuffs does at the compile time for a typical slowdown of 2-3 times. As with Wuffs there is no allocation in the basic Wasm, the program works on pre-allocated buffers.
Re: Wuffs’ PNG image decoder
#58why did the title change on this submission? is it not the fastest in the world?
The title changed multiple times. I've seen at least 3 in the last 30 minutes (safest, fastest and now this one).
Re: Wuffs’ PNG image decoder
#59First time hearing about Wuffs. It says Wuffs compiles to C. In this case, will the choice of C compiler affect the performance?
Re: Wuffs’ PNG image decoder
#60Looks good, but has somewhat widely false claims:
> SMHasher is a test and benchmark suite for a variety of hash function implementations. It can provide data for claims like “our new Foo hash function is faster than the widely used Bar, Baz and Qux hash functions”. However, when comparing Foo to CRC-32, be aware that a SIMD-accelerated CRC-32 implementation can be 47x faster than SMHasher’s simple CRC-32 implementation.
In fact smhasher implements both, the slow soft crc32 he cites, and the fastest crc32_pclmul, which is not just 47x faster, but 5000x faster. Other than wuff's implementation of the crc32_pclmul variant.
Compare https://github.com/rurban/smhasher/#smhasher
crc32 392.10 vs crc32_pclmul 1972140.38 MiB/sec