3 ms·

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 guarante

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.

aw1621107 6y ago
> 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.
- matu3ba 6y ago
  Checked as well. They can only do this, because they require that heap memory owned by pointers does not get fragmented. So programmers must manage pointer offsets to each heap structure themself. Hence you never get potential pointer soup (pointers pointing to subparts and pointing to other things), which Rust resolves with pointer lifetime checking. 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.
  - nigeltao 6y ago
    > programmers must manage pointer offsets to each heap structure I'm sorry but I don't understand this statement. Can you re-phrase it? > I would be more interested how they plan to handle IO effects or if they want to omit that. I'm not sure exactly what you're asking for, but see the Coroutines, Effects and I/O pages in https://github.com/google/wuffs/tree/main/doc/note https://github.com/google/wuffs/tree/main/doc/note
sanxiyn 6y ago
Wuffs does not use a SMT solver. https://github.com/google/wuffs/blob/main/doc/note/assertions.md https://github.com/google/wuffs/blob/main/doc/note/assertion... explains.
nigeltao 6y ago
> Are there any compiletime benchmarks? It used to take a couple of seconds to compile Wuffs' standard library. It's back down to a few hundred milliseconds. https://nigeltao.github.io/blog/2020/dumbindent.html#compilation-times https://nigeltao.github.io/blog/2020/dumbindent.html#compila...

aw1621107 6y ago

> 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.

matu3ba 6y ago
Checked as well. They can only do this, because they require that heap memory owned by pointers does not get fragmented. So programmers must manage pointer offsets to each heap structure themself. Hence you never get potential pointer soup (pointers pointing to subparts and pointing to other things), which Rust resolves with pointer lifetime checking. 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.
- nigeltao 6y ago
  > programmers must manage pointer offsets to each heap structure I'm sorry but I don't understand this statement. Can you re-phrase it? > I would be more interested how they plan to handle IO effects or if they want to omit that. I'm not sure exactly what you're asking for, but see the Coroutines, Effects and I/O pages in https://github.com/google/wuffs/tree/main/doc/note https://github.com/google/wuffs/tree/main/doc/note

sanxiyn 6y ago

Wuffs does not use a SMT solver. https://github.com/google/wuffs/blob/main/doc/note/assertions.md https://github.com/google/wuffs/blob/main/doc/note/assertion... explains.

nigeltao 6y ago

> Are there any compiletime benchmarks? It used to take a couple of seconds to compile Wuffs' standard library. It's back down to a few hundred milliseconds. https://nigeltao.github.io/blog/2020/dumbindent.html#compilation-times https://nigeltao.github.io/blog/2020/dumbindent.html#compila...