Are you making a joke with linking to “sound systems”? idgi :(
But also it’s false that a sound system isn’t a sound system. A sound system isn’t a complete system, which is a very different property!
I call these holes “soundless”, since they are neither sound nor unsound.
The hole itself isn’t “sound nor unsound”, soundness is a property of the logic. It’s like saying “5 is not an imperative programming language.” Values aren’t languages, languages are languages.
Lately, I’ve been tilting at “irresponsible” servers. If servers could offer guarantees about uptime/protocol, correctness could percolate down to my program at compile time.
You may be interested in “session types”, which are meant to offer protocol guarantees across programs. Still a research field but we might see them in production in a decade or two. Sadly uptime guarantees are (probably) statically impossible; you can’t typecheck away an asteroid strike!
Are you making a joke with linking to “sound systems”? idgi :(
Yes, it was a bad joke – I will update it for clarity.
The hole itself isn’t “sound nor unsound”, soundness is a property of the logic. It’s like saying “5 is not an imperative programming language.” Values aren’t languages, languages are languages.
Good catch. Can I say the hole is “soundless wrt its system”? Kinda like saying that S is independent of F?
You may be interested in “session types”, which are meant to offer protocol guarantees across programs. Still a research field but we might see them in production in a decade or two. Sadly uptime guarantees are (probably) statically impossible; you can’t typecheck away an asteroid strike!
You are spot on! My next post on this topic will be a brief comparison of session types, temporal type theory, TLA+, and a few other tools.
Your amazing TLA+ guide has been super helpful btw! Anybody reading this comment should buy your book :)
Are you making a joke with linking to “sound systems”? idgi :(
But also it’s false that a sound system isn’t a sound system. A sound system isn’t a complete system, which is a very different property!
The hole itself isn’t “sound nor unsound”, soundness is a property of the logic. It’s like saying “5 is not an imperative programming language.” Values aren’t languages, languages are languages.
You may be interested in “session types”, which are meant to offer protocol guarantees across programs. Still a research field but we might see them in production in a decade or two. Sadly uptime guarantees are (probably) statically impossible; you can’t typecheck away an asteroid strike!
Hi Hillel!
Yes, it was a bad joke – I will update it for clarity.
Good catch. Can I say the hole is “soundless wrt its system”? Kinda like saying that S is independent of F?
You are spot on! My next post on this topic will be a brief comparison of session types, temporal type theory, TLA+, and a few other tools.
Your amazing TLA+ guide has been super helpful btw! Anybody reading this comment should buy your book :)