<mq32>
andrewrk: i really find it interesting how superior some Rustaceans are. "rust is superior and all other languages are crap" or similar is the term i heard by a lot of people now and i find this saddening
<mq32>
*Rusteceans -(are) +(feel)
_Vi has quit [Ping timeout: 246 seconds]
_Vi has joined #zig
<_Vi>
By the way, Python - pythonista, Rust - rustacean, Zig - ?
* earnestly
.oO(lol)
* earnestly
refraims
<torque>
I don't understand people's incessant need to label themselves
<torque>
I don't think there's an reason to come up with a descriptor that implies some sort of allegiance to a specific programming language
<torque>
I think it's weird and polarizing to do this actually, and I actively dislike it, thats my 2 cents thanks
<Snektron>
whats the point of a mascot for a programming language
<daurnimator>
Snektron: plushies to sell? ;)
<daurnimator>
Snektron: but also, people found go more approachable due to their use of the gopher in docs.
<mq32>
Snektron, makes a nice impression and it's cool :D
_Vi has quit [Quit: _Vi]
Ichorio has joined #zig
samtebbs has joined #zig
<via>
oats: do you have that up anywhere? i remember trying and failing to just do a miniblink style gpio on/off without c wrappers, so i'm interested in how you might have gotten it to work
<samtebbs>
Should you 100% not be able to pass a `*std.io.seekable_stream.SeekableStream(std.os.SeekError,error{Unseekable,Unexpected,SystemResources,})` as a `*std.io.seekable_stream.SeekableStream(anyerror,anyerror)`, or is that a missing implicit cast?
<samtebbs>
It means I have to create annoying boilerplate that wraps the more specific stream
Demos[m] has quit [Read error: Connection reset by peer]
fengb has quit [Remote host closed the connection]
jzck has quit [Remote host closed the connection]
vegai has quit [Remote host closed the connection]
D3zmodos has quit [Remote host closed the connection]
Snektron has quit [Remote host closed the connection]
BitPuffin has quit [Read error: Connection reset by peer]
dtz has quit [Read error: Connection reset by peer]
BitPuffin has joined #zig
n_1-c_k has quit [Read error: Connection reset by peer]
n_1-c_k has joined #zig
Demos[m] has joined #zig
dtz has joined #zig
fengb has joined #zig
D3zmodos has joined #zig
jzck has joined #zig
vegai has joined #zig
waleee-cl has quit [Quit: Connection closed for inactivity]
_Vi has joined #zig
<daurnimator>
samtebbs: why shouldn't you be able to?
<daurnimator>
samtebbs: shouldn't std.os.SeekError cast implicitly to anyerror?
Snektron has joined #zig
porky11 has quit [Ping timeout: 245 seconds]
<samtebbs>
daurnimator: That doesn't seem to be the case unfortunately
<kenaryn>
Hi people. Please does someone know how metabuild are defined? For example, I am using zig 0.5.0+dca6e74f's version; is 'dca6e74f' the last commit's date encrypted in hexadecimal format? Or is it more complicated than that?
<mikdusan>
it's git commit hash from master branch
<mq32>
it's OpenGL ES 2.0, all written in Zig except for SDL
<scientes>
there is just a bunch of code I don't really understand
<mq32>
what's it about?
<scientes>
taking the address of a vector is special
<scientes>
&a[0]
<scientes>
but you can only tell if it is a vector after types have been resolved
traviss has quit [Quit: Leaving]
Akuli has joined #zig
<scientes>
there should be a way to get zig to not include a bunch of boiler plate and just look at the file provided, so that it is easier to use the debugger
<scientes>
its hard to filter out all the debugger noise
<earnestly>
If perfect software is software that is proven is true then no software is perfect
<earnestly>
But you can proof the provable parts, and although that proof doesn't compose, it does provide some trust
<companion_cube>
earnestly: there exists proven software
<companion_cube>
of course you can mistrust the prover, but well, it's still way better
<companion_cube>
(and way more effort)
<earnestly>
Formally verified software exists, and that software still fails when it assumes the network is perfect. They of course have far less bugs than unverified software so it's not for nothing
<companion_cube>
why would it assume the network is perfect?
<earnestly>
When you do formal verification you have to make sweeping assumptions about the environment, about state
<companion_cube>
it's clearly not for nothing indeed.
<companion_cube>
yeah, although for a C compiler like compcert, these assumptions are quite minimal
<fengb>
Formally verified architecture exists. I don’t believe implementations have been proven
<earnestly>
companion_cube: When verifying a system you can only do small parts of it as to verify it completely would require you verify everything about its environment as well as proof does not compose
<earnestly>
And the only programs which can be proven are total
<companion_cube>
tbh I think distributed systems are intrinsically harder
<earnestly>
What robust, resilient software does, is as the article I linked describes. You design error recovery subsystems (i.e. erlang, NASA's curiosity, etc.) and then throw as many adhoc formal methods as you can stomach at it
<companion_cube>
but stuff like memory bugs, array offsets errors, etc. are provable (http://why3.lri.fr/ eg)
<earnestly>
companion_cube: rowhammer
<companion_cube>
well if your point is that no software can be perfect, I think I agree
<earnestly>
Right, I'm trying to emphasis that it's not a silver bullet which I think you know, but sometimes forget
<earnestly>
emphasise*
<companion_cube>
it's just that it gets you 99.9% of the way
<companion_cube>
unlike tests, which may get you 50% of the way or something like that
<earnestly>
Resilient software, or even "progress oblivious" software is also programmed in ways utterly alien to normal software too
<companion_cube>
erlang like stuff is resilient only as much as the VM is correct, and writing a safe VM is more what Zig would/should excel at
<companion_cube>
(like, writing a flawless GC — and there you can't just recover)
<earnestly>
You can make Haskell software segfault by making the available stack size too small. All formally verified software has axioms, i.e. "assumed, tacit", etc. Sometimes those axioms are wrong, but even in mathematics, almost never questioned
<companion_cube>
hmm a Coq proof shouldn't contained "assumed" at all
<earnestly>
You have to, it would be too costly otherwise
<companion_cube>
hmm, no?
<companion_cube>
(as for the stack size, well, you can prove "terminates with correct result or crashes", which is a lot better than "anything goes because there might be UB")
<earnestly>
You can't prove that, that's the point. You'd have to solve the halting problem
<companion_cube>
wrong.
<earnestly>
(You can formally reason about it though, and that's good to do anyway)
<companion_cube>
you just have to prove the halting problem *in that particular case*
<earnestly>
Sure but your inputs are arbitrary
<companion_cube>
well, still ?
<companion_cube>
you can prove that `λx. x+1` terminates, whatever x is ;)
<companion_cube>
you can prove that a sort function terminates
<earnestly>
Not when composed
<companion_cube>
sure
<mikdusan>
plumm: that has to do with result-location semantics and it's part of setting it up. but i admit not having grok'd how that works yet
<earnestly>
Well, not without proving the composion
<companion_cube>
the halting problem just prevents you from writing an algorithm that always decides termination
<companion_cube>
yeah but that's what people do
<companion_cube>
that's what compcert does
<companion_cube>
(besides, here whitequark wasn't talking about proving correctness, but safety, which is less hard)
<earnestly>
companion_cube: Well they are working on certifying coq, so we'll see
<companion_cube>
ah, different thing, they're building another compiler. That's cool, a bit like cakeML, I guess.
<companion_cube>
impressive team, too.
<kenaryn>
earnestly perhaps you would be interested by F#, which is a formal concept-proof aiming at Coq replacement, and became a general purpose language. See more at: https://www.fstar-lang.org/
<companion_cube>
you mean F* ? yeah…
<earnestly>
I read F# and thought you meant F#, :P
<kenaryn>
It involves Inria once again, like companion_cube talked about compcert
<kenaryn>
nope... I said F*
<earnestly>
All of this stuff comes from inria
<earnestly>
F**
<companion_cube>
(I'm just talking about the stuff I know)
<kenaryn>
and I'm grateful for that, I added your links in my browser's favorites.
<kenaryn>
sorry, it was F* from the beginning, not F#. I mispelled it. :)
<kenaryn>
There is also another formal language to query a database and composed of structures embedded in the data itself, it is a direct concurrent of GraphQL, it is nammed Category Query Language.
<kenaryn>
But unlike the former one, it is under a company's control which is in charge of the IDE intrisically associated with CQL.
wootehfoot has quit [Read error: Connection reset by peer]