wuffs

I think Puffs looks like a cool new project: https://news.ycombinator.com/item?id=15711767 Edit: Looks like it was renamed to Wuffs: https://github.com/google/wuffs It's a domain-specific language for parsers that should be fast and must be correct, and it includes relatively light-weight verification.

I'm considering a name change: https://groups.google.com/d/topic/puffslang/cSrH-s7UqwA/disc... As for the "We're google, we can pick any name we want" assumption that somebody else wrote earlier, https://github.com/google/puffs says "Disclaimer: This is not an official Google product, it is just code that happens to be owned by Google". Also, before the launch, I didn't find many hits for "puffs" when searching github.com projects, or searching "apt search puffs", or searching the Web in general for queries like [puffs programming], or uses of the ".puffs" file extension. It's not like I cackled maniacally as I deliberately screwed over the NetBSD puffs project, whether for myself or on behalf of Google, I just didn't find it. I am bad at searching. Sorry.

I'm not entirely sure what you had in mind, but you can express certain inequalities. For example, https://github.com/google/puffs/blob/master/std/gif/decode_l... has this line: assert n_bits < (width + 8) via etc The 'via' syntax is discussed at https://github.com/google/puffs/blob/master/doc/puffs-the-la...

> I guess they’ve seen one too many bugs from precedence confusion. Yep. I just filed a precedence bug at https://github.com/jbangert/nail/issues/7 for Nail, which is a security-concious project. (It was presented at LangSec 2014). > It doesn’t have dependent types. Yep. Programming language theorists love type systems, and dependent types are one way to prove bounds safety, but they're not the only way. Puffs is an imperative language, not functional (for the reasons described in https://github.com/google/puffs/blob/master/doc/related-work...). With mutable state, a Puffs variable's within-bounds-ness can change over that variable's lifetime, but its type does not. > There is limited effect typing: functions can be marked pure, impure (!), or impure coroutine (?). Yep. That's the current design, although I'll probably revise that based o

Hi, Puffs author here. ingve linked to the github page instead of the announcement e-mail: https://groups.google.com/forum/#!topic/puffslang/2z61mNTAMn... That announcement has more to say about the comparison to Rust, which is probably the most frequently asked question. There's also some more words, on Rust and on other related work like Dafny, at https://github.com/google/puffs/blob/master/doc/related-work... Edit: It's also not Rust per se, but the numbers at https://github.com/google/puffs/blob/master/doc/benchmarks.m... shows that, on Puffs' benchmarks, gcc 7.2 noticably outperforms clang/llvm 5.0. I'm sure this is a solvable problem, and not a fundamental flaw with llvm, but fixing that's beyond my llvm knowledge.

Looks like it is not a general system, they prove the hardcoded binary operations: https://github.com/google/puffs/blob/master/lang/check/asser...

Good read so far: https://github.com/google/puffs/blob/master/doc/puffs-the-la...