IRC channel logs

2024-08-15.log

back to list of logs

<jfred>Whoa, I didn't realize how much stuff had made it into libadwaita. This is giving me ideas for GTK Guile apps with g-golf...
<cwebber>o/
<dckc>weary-traveler, the ingredients for language-level capability security are (1) Memory safety and encapsulation and (b) Primitive effects only via references. These are spelled out on https://monte.readthedocs.io/en/latest/intro.html#object-capability-discipline
<dckc>guile could perhaps do it with a new loader that doesn't expose things like `(display)`
<dckc>ACTION reboots workstation...
<weary-traveler>sneek: later ask dckc thanks for the monte reference. wouldn't control flow effects need to be handled as well, in addition to things like IO? it seems the requirements are for code to be functionally pure, and for side-effects to happen in some sense monadically
<sneek>Got it.
<fr33domlover>o/ haven't peeked here in a long time, so wanting to say hi ^_^ been following Spritely with excitement
<fr33domlover>My NLNet grant includes an actor programming system implementation in Haskell
<fr33domlover>And it's more and more becoming the focus of my work
<fr33domlover>It still needs stuff like promise pipelining and networking, to be anywhere near what Spritely does, but I intend to model is after Goblins and implement OcapN
<fr33domlover>I'll probably be reusing Ian's CapnProto Haskell implementation (which I'm proud to do becaue he also mentored me on lots of OCAP stuff), as well as an incomplete OcapN-in-Haskell implementation that has been abandoned
<weary-traveler>fr33domlover: you mean the ocap-io library?
<weary-traveler>it seems to have been by the same ian
<fr33domlover>weary-traveler: I mean literally the Cap'n Proto implementation in Haskell, idk if it's on Hackage but capnproto.org probably has the link :)
<fr33domlover>Perhaps it uses cap-io as a dependency though
<weary-traveler>fr33domlover: the capnproto haskell port is called capnp. it's on hackage
<weary-traveler>sneek: later tell dckc oh and in guile, you'd also need to get rid of global variables and mutability in order for it to be capability-safe
<sneek>Got it.
<dthompson>fr33domlover: there are some people that have been trying to implement ocapn for haskell. maybe you could join in this effort??
<dthompson>weary-traveler: functional purity is not a prerequisite for capability-safe programming. nothing wrong with stateful effects as long as you have been given the capability to perform them.
<dthompson>example: a webassembly module that imports a mutable global.
<weary-traveler>dthompson: functional purity is an overloaded term, so let's be precise. what i meant is that it's necessary to be able to outlaw things such as shared state. mutability is not problematic, but unguarded mutability of globals would be. do you disagree?
<dthompson>that sounds about right
<fr33domlover>dthompson: Last time I asked, they abandoned that effort, but I hope to pick it up or at least reuse what they did before they stopped
<dthompson>fr33domlover: that's unfortunate but I'm glad that you want to pick it up!
<dthompson>we have monthly meetings if you'd like to attend in the future
<weary-traveler>dthompson: since i don't know about webassembly, what language facilities does it provide to be able to distinguish "pure" code from "impure"? or is it the manner in which the wasm code is being generated that makes it possible to keep these apart?
<dthompson>if I understand you correctly, there's no such distinction
<weary-traveler>btw, i have found murray's thesis quite informative and helpful (more so than miller's, though the latter is perhaps better if the goal is to gain some intuitive familiarity)
<dthompson>but the type system has mutable and immutable variants for certain things
<weary-traveler>dthompson: okay, then i'm not sure what you meant that goblins would get language-level capability security via wasm. hopefully i'm not misremembering you
<dthompson>I'm just using wasm as an example of a capability-secure environment that has mutability
<dthompson>a wasm module can only utilize the resources given to it by the host at instantiation time.
<dthompson>be it globals, functions, memory, etc.
<weary-traveler>i see. inter-module security. as opposed to intra-module. thank you that helps
<dthompson>it also has "intra-module" security when it comes to wasm gc. if you don't have a reference to a heap object, you can't conjure one up.
<dthompson>it's memory-safe
<weary-traveler>memory-safety is necessary, but are you saying that it's sufficient (without being able to distinguish code that can or can't modify some "undeclared" shared state) for proving some security properties (e.g., liveness, information flow etc.)
<dthompson>there can't be any undeclared shared state.
<weary-traveler>oh i see
<dthompson>guile is full of ambient authority things, like the entire posix api.
<dthompson>a "safe guile" could not provide direct access to any of that
<weary-traveler>yeah, that matches my understanding
<dthompson>guile's 2 biggest problems here are 1) enormous default environment with the posix api and 2) any module can import any other module on the load path
<weary-traveler>i see, the perspective, once again being regd. inter-module security. yeah modules in lisps are more like namespaces without encapsulation
<dthompson>if we can get some funding for a safe scheme on guile we will work on this
<dthompson>I think a lot of inspiration can be taken from wasm. and of course lexical scope is already the perfect language foundation.
<weary-traveler>how would you distinguish safe code from unsafe? have a compiler phase that complains, perhaps?
<dthompson>idk what the interface might look like, but something like the js api for wasm might work. the host (running regular guile) could instantiate a safe scheme program, passing along the necessary imported capabilities
<dthompson>the safe program would be compiled in a context where none of the dangerous stuff is lexically bound
<weary-traveler>the safe program would need a modified compiler to ensure no violation of inter-module boundary
<dthompson>the general idea would be to re-use guile's existing compiler. safe scheme would compile to scheme.
<dthompson>the frontend for safe scheme would do whatever it needs to do and lower to plain scheme
<weary-traveler>yes, hence modified compiler :) i suppose one can argue that an addition of a separate compilation pass doesn't make a new compiler, but lines get blurred there since safe scheme would be a strict subset of scheme
<dthompson>yeah okay seems we're on the same page :) just wanted to be clear that guile's extensible compiler tower makes it so we don't have to forego all the compiler goodness that guile already has
<dthompson>I've made small languages that lower to scheme before. it's fun.
<weary-traveler>do guile modules only ever get distributed as source? if not, then it'd be necessary to be able to tell a compiled safe module from an unsafe one
<dthompson>guile would need additional work to support running safe programs as bytecode. I think source-only would be the first step.
<weary-traveler>EDSLs are indeed fun. of course one also has the option to consider that what constitutes a module boundary in safe-scheme, isn't the same thing in regular-scheme
<dthompson>the module system would have to be entirely different, yeah.
<dthompson>guile modules are too loose about where stuff comes from. r6rs style (and I think r7rs) is explicit, though.
<dthompson>well, more explicit. you still can say (import (scheme base)) without saying *what* you want to import from it.
<dthompson>but you can't transparently have duplicate definitions that shadow each other like define-module allows, bleh
<dthompson>my gut feeling is that being explicit about which names are imported and which names are exported is a prereq for a safe scheme module system.
<dthompson>and it would resolve a common complaint people have about scheme while we're at it ;)
<weary-traveler>it would have to be explicit, because if it allowed a way to access members without them being explicitly stated all guarantees go out the window
<dthompson>yeah exactly
<dthompson>(and it just makes sense for readability, even thought it's annoying sometimes)
<dthompson>though*
<weary-traveler>idk, the export lists shouldn't be too long (and if they are, good indication for the module to be split). the import list would have to be a subset, but given decent export list, the burden on the caller wouldn't be much