Posts tagged with #provingthecodinginterview
-
Leaning into the Coding Interview 4: Certified Programming with Proof-Carrying Code
Migrating from `List` to `Vector` paid dividends for us being convinced that our Fizzbuzz implementation was correct. Does making our `FB` value type dependent also increase our confidence of correctness?
-
Leaning into the Coding Interview: proving equality of different Fuzzbuzzes
There are lots of different ways to implement Fizzbuzz but this one is mine - how can we prove different implementations are actually the same, and what does it look like when they're actually not?
-
Leaning into the Coding Interview 3: completing our spec with tacticals and metaprogramming
Time to actually write our end-to-end specification!
-
Leaning Into the Coding Interview 2: static bounds checks and dependent types
Pls types? No terms! Only (indexed, dependent) types!
-
Leaning Into the Coding Interview: Lean 4 vs Dafny cage-match
Is Fizzbuzz easier to write in Lean, or just differently hard?
-
Proving the Coding Interview: verifying the JDK's `Integer.toString()`
A faster, but just as correct, nat -> string converter
-
Proving the Coding Interview II
Integer.toString() 2 furious
-
Proving the Coding Interview
Applying interesting research to uninteresting interview problems