I am told that final design of bend2 resolves second question neatly. Progress is real.
Regarding first question / comment: Still will need a lot of native re-implementation (and even then will need many lower level libraries with ffi’s) OR approach it similar to how urbit tried to explain “exhaustive testing” of underlying jet to establish a set of “proven behaviors” in release ver of programs using effectively a “short-hand” that’s outside of formal proof system (needs to be just accepted). Now, urbit’s hoon was never a language meant for formal verification, so interested in seeing how bend2 tackles it.
These are just my intuitions. I haven’t really played with bend2 yet.
Regarding first question / comment: Still will need a lot of native re-implementation (and even then will need many lower level libraries with ffi’s) OR approach it similar to how urbit tried to explain “exhaustive testing” of underlying jet to establish a set of “proven behaviors” in release ver of programs using effectively a “short-hand” that’s outside of formal proof system (needs to be just accepted). Now, urbit’s hoon was never a language meant for formal verification, so interested in seeing how bend2 tackles it.
These are just my intuitions. I haven’t really played with bend2 yet.
@VictorTaelinThanks.
> equivalent effects
So if I wanted to use a library for kafka, it would have to be native bend2 kafka library instead of target lang’s library. Since you’d have to produce proof. Ok, got it.
> Bend2 is meant to be a disposable language
but most of the errors are due to functions across different file scopes, forgive me for being stupid here, so bend2 isn’t intended for that? At unit level in that case would work fine, but if transpiled code’s usage of a function for instance has not changed, then ai makes change to function, and that function passes bend2 muster, you’d still have error. Or am I retarded and just talking about a trivial case here?
Thank you kindly
Oct 24, 2026 · 9:44 AM UTC
0
0
0
100