fp likers: what were you doing the first time you thought fp was good

The Something Awful Forums > Discussion > Serious Hardware/Software Crap > YOSPOS > fp likers: what were you doing the first time you thought fp was good

Bloody: Mar 3, 2013

Symbolic Butt posted:

fp made me aware of managing state better, before that I was just like yolo

Plank Walker posted:

linq is pretty nice i guess

# ¿ Nov 20, 2017 22:27

Adbot: ADBOT LOVES YOU

# ¿ May 10, 2024 17:49

Bloody: Mar 3, 2013

atomicthumbs posted:

if your software isn't formally verified, go gently caress yourself

just say "formal methods" a lot nobody knows what it means

# ¿ Nov 21, 2017 01:24

Bloody: Mar 3, 2013

`ls` stands for `locate poo poo`

# ¿ Nov 21, 2017 01:36

Bloody: Mar 3, 2013

Star War Sex Parrot posted:

hell yeah check out the sweet invariants I wrote for my hash table

code:

  type hashtbl 'a = {
    mutable size: int ;
    mutable data: data 'a ;
    ghost mutable model: model 'a }

    invariant { length self.data > 0 }
    invariant {
      forall u:key. forall v:'a.
      mem (u, v) self.data[bucket u (length self.data)] <->
      Map.get self.model u = Some v }
    invariant {
      forall u:key. forall v:'a. forall w:'a.
      (mem (u,v) self.data[bucket u (length self.data)] /\
      mem (u,w) self.data[bucket u (length self.data)]) ->
      v = w }
    invariant {
      forall i: int. 0 <= i < length self.data ->
      forall u: key, v: 'a. mem (u,v) self.data[i] ->
      bucket u (length self.data) = i }

proving these during resize was sort of a bitch. this is the signature and contracts for a resize function whose body is like 6 lines

code:

    let rec rehash (new_data : data 'a) (l : bucket 'a) (ghost i : int) : unit =
      requires {
        forall j: int. 0 <= j < new_size ->
        forall u: key, v: 'a. mem (u,v) new_data[j] ->
        bucket u new_size = j }
      requires {
        forall u: key, v: 'a. mem (u,v) l ->
        bucket u old_size = i }
      requires {
        forall u:key. forall v:'a.
        0 <= bucket u old_size < i ->
        (mem (u, v) new_data[bucket u new_size] <->
        Map.get t.model u = Some v) }
      requires {
        forall u:key. forall v:'a.
        bucket u old_size = i ->
        (Map.get t.model u = Some v <-> mem (u, v) l \/
        (mem (u, v) new_data[bucket u new_size])) }
      requires {
        forall u:key. forall v:'a.
        bucket u old_size > i ->
        not (mem (u, v) new_data[bucket u new_size]) }
      requires { new_size = length new_data }
      ensures {
        forall j: int. 0 <= j < new_size ->
        forall u: key, v: 'a. mem (u,v) new_data[j] ->
        bucket u new_size = j }
      ensures {
        forall u:key. forall v:'a.
        0 <= bucket u old_size <= i ->
        (mem (u, v) new_data[bucket u new_size] <->
        Map.get t.model u = Some v) }
      ensures {
        forall u:key. forall v:'a.
        bucket u old_size > i ->
        not (mem (u, v) new_data[bucket u new_size]) }
      variant { l }

idk what any of that means tbh

# ¿ Nov 21, 2017 01:42

Bloody: Mar 3, 2013

Star War Sex Parrot posted:

languages like F* and WhyML allow you to specify contracts with first order logic, and then automated provers can formally verify whether the code actually matches the specification

it's neat I guess but still feels largely academic to me

yeah i mostly have no idea how to mentally parse and interpret the contracts

# ¿ Nov 23, 2017 00:14

The Something Awful Forums > Discussion > Serious Hardware/Software Crap > YOSPOS > fp likers: what were you doing the first time you thought fp was good