Conversation

Quil (キュー)
@robotlolita
A counterpoint to this is that UB is not an empowering tool to users; we're shifting the burden of verifying optimisations to users *without* giving them any tools to do so. And it always comes back later to bit the users, not us. We need better alternatives here!
Quote Tweet
ACM SIGPLAN
@sigplan
·
Undefined behavior can get a bad rap. Applied judiciously, however, it’s a critical tool for letting compilers optimize low-level code while keeping programmers in control. blog.sigplan.org/2021/11/18/und
1
9
Quil (キュー)
@robotlolita
Crochet, being a security-oriented language, cannot have something like UB for example. Even trusted FFI is problematic. So my current idea is to have little languages users can extend compilers for at local contexts, providing their own proofs, as a tool to the same end.
2
3
Brendan Zabarauskas
@brendanzab
Oh nice! I think this is where they are trying to head with RustBelt? Alas it's a big leap from writing rust code too constructing an Iris proof with Coq… I wish the barrier to entry were lower… I'm excited to see what it would look like if it were built in from the start.
1
1
Quil (キュー)
@robotlolita
Didn't know about RustBelt, but yeah, seems that it was going in that direction. But yeah, proving things is hard, and I'm not sure how to approach that for things like concurrency. Crochet currently goes in a direction more like Dafny, which mostly deals with bounds and stuff.
1
2
Brendan Zabarauskas
@brendanzab
Ahh cool (was worried I was just mentioning stuff you were already aware of). If your curious about more on this stuff, you might find this post interesting, about integrating ‘syntactic type soundness’ with ‘semantic type soundness’:
blog.sigplan.org
What Type Soundness Theorem Do You Really Want to Prove?
For decades, researchers have syntactically proved type soundness to establish their type system works. This post shows why a semantic notion of type soundness is more appropriate, for covering abs…
1