Viewing profile — quietusmuris
quietusmuris
HN member- Joined
- Thu, Jun 18, 2026, 1:31 PM UTC
- HN karma
- 8
- Public activity
- 3 items
- HN profile
- View on Hacker News ↗
About quietusmuris
No profile information was provided.
Recent public activity
-
comment
Comment #48617864
So the compiler's in the Trusted Base either way and the asserts are just part of the spec surface the user has to get right. Makes sense.
-
comment
Comment #48599110
Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?
-
comment
Comment #48588358
Interesting. Do I have to write specs in Lean against the Wasm semantics or can you annotate Rust directly?