Andrew Boyton

Christian. Father. Developer. Principal Software Engineer at @theiconicau Previously @kayosports @freelancer. PhD in formal methods.

[Andrew Boyton @boyto_]

@aarondfrancis @1stevengrant @IanLandsman I don’t know what you mean by faith AI podcast but this book won Australian Christian book of the year last year and @MrSteveDriscoll has been on a few podcasts about it (and is visiting my church next month). https://t.co/tM7G64lmm2

[Andrew Boyton @boyto_]

@thdxr No.

But I also try ban reduce in product code and try make library functions that wrap it.

I find it way too easy to accidentally make quadraticn reduce functions with object spread. Mostly I find named functions easier to read. Just waiting for the pipe operator for ergonomics

[Andrew Boyton @boyto_]

@kitlangton Nice. Any idea how this compares to jj spr?

[Andrew Boyton @boyto_]

@mpgros @jamonholmgren Mutation testing feels like it would make your tests more coupled, but given how often I've seen it recommended I think there's something I don't understand that I just need to try, especially on sociable tests.

https://t.co/MbDF856tKf

[Andrew Boyton @boyto_]

@mpgros @jamonholmgren Right now I’ve seen a fascination of test coverage at the expense of confidence, where you write shallow/solitary unit tests that just match your implementation, and then you have a bug and it passes all your tests.

[Andrew Boyton @boyto_]

@mpgros @jamonholmgren I made a PR yesterday at work to introduce a new type of UI tests that use in-memory fakes at the network boundary rather than shallow static mocking. I’ll try PBT next. I find AI is great at hallucinating mocks that make test pass, not that bring confidence. Fakes should help.

[Andrew Boyton @boyto_]

@thdxr No different from operating systems. They kill all many of things.
https://t.co/nZy69beddO

[LaurieWired @lauriewired]

OS internals books are wild...

[Andrew Boyton @boyto_]

@capemox @potetm I definitely hated that part of go. Very few data structures and for loops everywhere.

I’d always assumed I was supposed to use a map of Booleans and than have to work out if i stored false or have it missing. I never considered empty strings.

[Andrew Boyton @boyto_]

@jocadbz As someone whose PhD was on a formally verified capabilities-based microkernel (and personally uses a Mac), and is a recent convert to jj, this post is incredible.

[Andrew Boyton @boyto_]

@JustDeezGuy @onehappyfellow Oh lean has a runtime that’s part of its TCB? That’s VERY different from the seL4 work on Isabelle or Rocq proofs. That really doesn’t seem ideal. https://t.co/3NXRMjvQRR

[Andrew Boyton @boyto_]

@JustDeezGuy @onehappyfellow What does this mean though when it comes to your original questions about the size of the TCB, human audit, etc. Aren’t Isabelle, Rocq and Lean reasonably similar for those? Or am I missing something?

[Andrew Boyton @boyto_]

@JustDeezGuy @onehappyfellow I thought even with de Bruijn/Curry-Howard you still had a somewhat similar thing with a small TCB, this time being the type checker (rather than a kernel) and the tactics write complex proof terms the checker checks. So very different underpinnings but similar results?

[Andrew Boyton @boyto_]

@JustDeezGuy @onehappyfellow I’ve been out for too long but I though Isabelle/HOL aimed for a small kernel for the TCB and then the tactics ran outside the kernel and didn’t have to be correct as they told the kernel what to do. Is Lean different here?

[Andrew Boyton @boyto_]

@davidcrespo @sameenkarim @github Been using jj spr for the last month. Absolutely love it. It’s finally come the closest to the Phabricator workflows that I used to love.

[Andrew Boyton @boyto_]

@zeeg Imagine if they were in-memory fakes not just static mocks. For many tools there’s 3rd party ones like this impressive reimplementation of MySQL in PHP, or countless Redis ones, but official ones would be great. https://t.co/nZ51fsqFMX

[Andrew Boyton @boyto_]

@halfedge @miketuritzin That article was fantastic thanks.

I often go to these two great articles about similar topics when needing to explain this but I’ll definitely be adding yours to my list.

https://t.co/VGOcwLF7ls

https://t.co/rwLPoUCrFm

[Andrew Boyton @boyto_]

@housecor Doesn’t this mean your website is also down during these times? I’d suggest this is uncovering useful information. Is there a way to wrap the 3rd party to make it more resilient or to replace it?

[Andrew Boyton @boyto_]

@kettanaito @kentcdodds Not just moving mocking to deeper in the call stack but also the idea of replacing static mocks with in-memory fakes. I find that’s the wow moment for people who over-mock. Takes a bit to set up but once you do. Incredible.

[Andrew Boyton @boyto_]

@damekdavis @tribbloid Isabelle/HOL had a method a decade or so ago that would try find counter examples. Wasn’t perfect but sometimes it was VERY helpful. Based on Haskell QuickCheck IIRC.