!JxzWpvsvfYuMHyUJiL:matrix.org

rust-ipfs

283 Members
Implementing ipfs in rust35 Servers

Load older messages


SenderMessageTime
18 Aug 2021
@server_stats:nordgedanken.devServer Stats Discoverer (traveler bot) joined the room.16:38:46
19 Aug 2021
@birkanm:matrix.orgBirkan M joined the room.09:50:47
20 Aug 2021
@dan.shields:matrix.parity.ioDan Shields changed their display name from Dan Shields to Dan (OOO, Support -> @alejandro-martinez:matrix.parity.io).05:08:34
@dan.shields:matrix.parity.ioDan Shields changed their profile picture.05:10:01
21 Aug 2021
@j.liebert:matrix.orgj.liebert joined the room.12:46:47
@0xdeadbeefonroad:matrix.org@0xdeadbeefonroad:matrix.org joined the room.21:26:28
22 Aug 2021
@0xdeadbeefonroad:matrix.org@0xdeadbeefonroad:matrix.org left the room.14:38:41
26 Aug 2021
@david:web3.foundationDavid - ooo until 24.09.21 changed their display name from David to David - ooo until 24.09.21.06:58:35
29 Aug 2021
@dvc94ch:matrix.orgdvc94chSo it's been a bit quiet, but that doesn't mean there was nothing going on10:04:13
@dvc94ch:matrix.orgdvc94chThe last few weeks I was formalizing a system for schema transformations in a decentralized network in idris10:05:15
@dvc94ch:matrix.orgdvc94chWhat makes it harder than in a centralized system is that you have to maintain forwards and backwards compatibility. In a centralized system you can update the servers and just have to be backwards compatible10:06:35
@dvc94ch:matrix.orgdvc94chNext week I'll be implementing it in rust and use coverage based fuzz testing for verifying the rust implementation10:07:59
@dvc94ch:matrix.orgdvc94chAlso working on extending the system to crdt operations and proving that a json crdt still converges after transforming it's ops10:08:52
@dvc94ch:matrix.orgdvc94chhttps://github.com/dvc94ch/fcrdt10:10:26
@cryptoquick:matrix.orgcryptoquickNice! Idris is really cool, and dependent types are badass. Have you thought of using a more formal proof for the distributed system, such as Leslie Lamport's TLA+? I don't have much experience with this, I just know it exists and it's supposed to be good for this.12:08:16
@dvc94ch:matrix.orgdvc94chI've dabbled in tla+ in the past. It has a couple of downsides. The specification is not executable, so it doesn't help you validate an implementation. It also makes it hard or impossible to validate the specification itself as in putting some values in and seeing if the result is what you wanted. It's too easy to create a model that checks, but has zero valid states.12:11:11
@cryptoquick:matrix.orgcryptoquickMakes sense. Idris is pretty good, then. Are you using Idris 2? It's crazy how it's supposed to just fill in your types with Chez Scheme. You're not writing code, only types. I also hear good things of Luna lang.12:14:06
@dvc94ch:matrix.orgdvc94chYes, using idris2. I'm planning to stick with it. The reason I chose Idris over coq/Isabelle is that I think it's much more accessible to engineers. I'm planning on adding new features in Idris first and then in rust, keeping the specification and proofs up to date12:16:37
@dvc94ch:matrix.orgdvc94chI think this is currently the most practical way of high assurance software development in rust12:18:10
@cryptoquick:matrix.orgcryptoquickThat's so awesome. I've looked at Haskell but it doesn't seem as interesting to me as Idris. Haskell seems old and clunky, especially the tooling, but Idris seems to offer more features, and I think it might even be faster.12:19:14
@dvc94ch:matrix.orgdvc94chWell Haskel doesn't let you do proofs. Idris is Haskel with proofs12:20:35
@dvc94ch:matrix.orgdvc94chAnd talking about clunky, coq/Isabelle are clunky and use ocaml also clunky for package management and program extraction. Idris is still very young and could use more funding/developers, but at least it's a single horse and not a collection of them to bet on12:23:02
1 Sep 2021
@dvc94ch:matrix.orgdvc94chhttps://github.com/actyx/cambria16:07:44
@dvc94ch:matrix.orgdvc94chCheck it out, it's zero copy intended to be used with zstd compression16:08:19
5 Sep 2021
@dan.shields:matrix.parity.ioDan Shields changed their profile picture.13:25:36
@dan.shields:matrix.parity.ioDan Shields changed their display name from Dan (OOO, Support -> @alejandro-martinez:matrix.parity.io) to Dan Shields.13:31:28
9 Sep 2021
@telegram_808949413:t2bot.ioAlex - Subsocial changed their display name from Alex - Subsocial Network to Alex - Subsocial.14:59:18
11 Sep 2021
@dvc94ch:matrix.orgdvc94ch
data History : List Op -> List Op -> Type where
    HNil : History [] []
    HSkip : (op : Op) -> lamport op >= lamport' xs = True -> History xs ys -> History (op :: xs) (op :: ys)
    HSwap : (op, op' : Op) -> lamport op = lamport op' -> lamport op >= lamport' xs = True ->
        History xs xs -> History (op :: op' :: xs) (op' :: op :: xs)
    HTrans : {ys : List Op} -> History xs ys -> History ys zs -> History xs zs

so had a break through with modeling the history. still will require some work to convince myself that it is the correct definition

convergence : (k : PrimitiveKind) -> (a, b : List Op) ->
    History a b -> reg_apply {k} a = reg_apply {k} b
convergence k [] [] HNil = Refl
convergence k (op :: xs) (op :: ys) (HSkip op prf h) =
    rewrite convergence k xs ys h in Refl
convergence k (op :: (op' :: xs)) (op' :: (op :: xs)) (HSwap op op' prf prf1 h) =
    reg_update_commutes k op op' (reg_apply xs) prf
convergence k a b (HTrans {ys} h h') =
    let c1 = convergence k a ys h
        c2 = convergence k ys b h'
    in rewrite c1 in rewrite c2 in Refl

but it allowed me to elegantly prove that the multivalue register converges provided that concurrent update operations commute

14:38:33
13 Sep 2021
@alejandro-martinez:matrix.parity.ioalejandro-OoO changed their display name from alejandro to alejandro-OoO.08:05:31
14 Sep 2021
@apopiak:matrix.parity.ioAlexander Popiak joined the room.15:14:04

There are no newer messages yet.


Back to Room List