Frankly speaking ...

I've been curious about dependent types for some time. After wrestling with them in Haskell , discovering Lean felt like a small revelation. Two weeks in, Lean's proofs-as-values and tighter types already feel like the missing piece I couldn't quite get in Haskell. My Haskell background helps; the language still feels familiar enough that the learning curve is manageable. In this post I compare two Word Puzzle solvers I implemented: one in Haskell and my first program in Lean 4 . Below I list the differences I noticed and why they mattered for design, validation and I/O. Overview of the Problem I built both projects to solve an identical problem: given a pool of 4–9 lowercase letters and a mandatory letter, filter a dictionary file for words that can be spelt from the pool. My Haskell version uses pull-based streaming I/O with the io-streams library and applicative validation via Data.Validation . For my Lean 4 attempt, I used dependent types with compile-time...

This post was first published on 15 October 2020, but that site has since been shut down. Part 1  of this series explored pseudo-random values—statistically random values derived from a known starting point. This article explores using random values in testing. Randomness in test invocation is common; for instance,  JUnit5  provides an annotation to  randomise the order of test execution . This article, however, examines a testing style using randomly generated input values to test  properties  of code, known as "Property-Based Testing". Why use random values in testing? Defining suitable positive and negative test cases to exercise code is often difficult. Automating the execution of many randomly selected tests covers a broader range of input values. Furthermore, recording and reporting failing tests allows for replay and debugging. Property-based testing verifies program code using a large range of relevant inputs by generating a random sample of valid v...

The following is a number of different methods you can use to strip ^M from files. This was more of an exercise than a feature I need regularly. However, there was a recent incident at work where someone had checked-in such an abomination. Some tools just don't like Windows line endings in files, i.e. CRLF, Carriage Return Line Feed . So, as an exercise, here is a collation of the numerous ways to fix these aberrations ... Note: Most editors now have a quick way of doing this. file You can see whether a file has ^M using the file command: Example Consider a file containing ^M, file reports: $ file test.txt test.txt: ASCII text, with CRLF, LF line terminators After stripping ^M, we have: $ file test-fixed.txt test-fixed.txt: ASCII text dos2unix Probably the simplest way is to use the dos2unix command. Example Show file has ^M line endings: $ dos2unix -i test.txt 3 16 0 no_bom text test.txt Now fix: $ dos2unix test.txt Proof that file has been fixed...