edef.txt ✅ @edef@mastodon.social

I'm now trying to learn ProVerif from the fine folks at Inria
http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
h/t @spun_off (https://twitter.com/spun_off/status/908695983156088832)
it seems to do exactly the kind of knowledge-modelling I want

the point is, I'm a dumbass, help me find tools that'll tell me in which exact ways I'm being a dumbass in protocol design, kthx

wait fuck TLA+ isn't the tool I was thinking of, *handwave* process calculus or something, urgh

I know of tools like TLA+ for modelling protocol interactions between agents, and all I'm adding here is a notion of (derived) knowledge, and I strongly doubt I'm the first to want this.

dear formal methods folk, is there a convenient tool for modelling agent-knowledge in (cryptographic) protocols that I should know of?
I've been playing around in Prolog a little (see image), but I'm sort of drawing a blank on how I'd properly model this. https://mastodon.social/media/5xooGPOV-Cm__VHC0kI

hey lazyweb, I'm looking for recommendations on free/libre UI mockup software
preferably stuff that looks more sketch-like, I'm not trying to depict the polished final product, because that tends to inhibit critique

what makes this all even funnier is that I'm starting to see a lot of the value of XML's extensibility mechanisms
sure, the attr/tag distinction is iffy, but namespaces and DTDs were an incredibly good move

"is this just RDF but with JSON"
"yyup"

current status: being way too entertained about how we're reinventing failed big dreams of the past with JSON instead of XML

I'm pretty shocked at how expensive internet pharmacies are? These folks must be making incredible margins on this stuff

okay that was enough yammering about overly serious shit, what's up Mastodon?

of course none of the synchronisation primitives actually compose well, other than channels (there's a single, rather inflexible `select` primitive)
so you end up reinventing a bunch of the `sync` package out of channels, or using additional goroutines to wrap them, though g'luck if you want cancellation in the latter case

my favourite feature by far is the I/O / concurrency runtime: it's solid as heck, you don't have to argue with people using some other concurrency framework because there isn't anything else you could or would want to use (node sort of has this)

I miss the shit out of Result/Either/etc style error handling, instead of having two nullable return values (no tuples, multiple return values!) that you get to check yourself
nor do you actually have any clue about what your errors look like at the type system level
enjoy your interface{Error() string} and checked downcasts

it's not all sunshine, obviously: I spend a tonne of time thinking about data ownership due to the lack of immutability, checked thread-safety, etc
nullable everything is a fucking scourge even though you can sometimes make clever use of it
the lack of enums / tagged unions is the absolute fucking worst and I spend too much time designing data structures because of it

I've found some value in the limited abstraction capabilities forcing me to build more concretely, instead of allowing me to build inappropriate abstraction boundaries with ease
It's really easy to mess that up in generic programming and never truly realise - I've been forced to clean up a lot of conflation of concerns early due to the lack of real generic programming.

the uniformity in Go code and project setups also ensures external code is easy to adopt and treat as your own, and thanks to having really solid editor tooling, exploring external code is something I do often and with pleasure