owi @owi@mastodon.social

#introduction time! I'm Oskar, and I spend most of my time online talking and writing about #programming, including but not limited to #Haskell and #FP, #testing, #architecture, #FOSS, #Linux, and #web. I have a blog at https://wickstrom.tech and I produce screencasts at https://haskell-at-work.com when there's time.

I also do #music, mostly acoustic #guitar nowadays, and only spare time.

See you around!

Or @hillelogram@twitter.com ?

@larrytheliquid@twitter.com perhaps? 😊

Anyone who can recommend a reference on implementing branching temporal logics, like for a model checker? Keen to find something concrete but preferably stripped down to its essentials (not a full implementation like TLC in the TLA+ Toolbox.)

A half-assed attempt at a clickbait description, at least! But seriously, read the thing.

The second case study in "Property-Based Testing in a Screencast Editor" is out!

Learn all about my silly bugs, how using PBT made them go away, and how you can enjoy the same humbling experience when testing your buggy code base.

https://wickstrom.tech/programming/2019/04/17/property-based-testing-in-a-screencast-editor-case-study-2.html

"The One Weird Trick To Find All Bugs That Evil Middle Management Don't Want You To Know About"

is this how it's done?

Good thing I'm not trying to make ad money on my blog because my titles are _boring_. Like dead serious silent northern European boring.

It's a lovely day in Malmö today; the sun is shining and I'm publishing my next PBT case study! ☀️👨‍🔬

I'm up way too early running way too many tests.

It's fantastic to get to apply this at work. I'm having loads of fun, finding bugs early!

I've been working on property-based integration testing at @SymbiontIO@twitter.com
for our CLI, running the application's commands and verifying
high-level properties like idempotency and resumability with fault
injection.

Property-based testing goes way beyond testing pure functions!

So the F* verifier might say "could not prove post-condition". I could at that point just stare at my code for a long time and hope I can figure it out. Or I can randomly change my functions, lemmas, and proof definitions. But maybe there are better ways?

I'm a noob in the formal verification PL space. Trying out F* and practicing writing proofs based on the tutorial.

Unsure if this is F* or a general problem: when I make a mistake the verifier says "no". How do I proceed? Are there tricks? How do I debug my lemmas and proofs?

Shout-out to https://github.com/nicholassaunders who's doing great work maintaining the PureScript Hyper and Trout libraries! 👏😍

Tonight: Pink Floyd and F* programming.

F* hacking in Emacs is slick!

Programming in Dafny is so fun! Nice to have formal verification accessible for noobs like me. 😀

Messing around with Dafny, trying to find my old bugs before they would've happened.

Anyone knows if there's already a way to do Maybe/Optional? Without references and null, I guess? I can define Maybe on my own, but there might already be something for it. Any standard lib?

Had a great day in Gothenburg at the Smart Testing meetup of #fossnorth2019. Glad to spread the joyful tales of property-based testing in industry programming. ☺️

Messing with the F* language a bit. It's fun and the tutorial is nice!