User settings, Lamport clocks and lightweight formal methods

jakub-m.github.io

21–22 of 22 posts

Re: User settings, Lamport clocks and lightweight formal methods

#21

Post by chriswarbo » Thu, Jul 21, 2022, 11:04 AM UTC

User23 wrote: post #3

Interesting. Incidentally, I would claim that TDD done properly is in fact a lightweight formal method. It helps to be conversant with some kind of formal semantics, but you can definitely play a bit fast and loose by treating your tests as a lightweight specification. In that case any formal properties I want the code to have that can't practically be expressed in the test is included in a comment on the test. Also,…

Property-based tests let us state the formal properties we want, even though we can't verify them. For example, ScalaCheck lets me state the following:

    forAll (x: Int) { assert(x.abs >= 0) }

This is useful as a spec, as documentation, and as a test suite: e.g. ScalaCheck can try to disprove such properties by checking a bunch of random inputs.

Whilst such approaches don't let us prove such statements (except for exhaustively checking small input spaces, e.g. `forAll (x: Boolean, y: Boolean) ...` only needs four tests), I find it just as easy as normal unit testing, and far less effort than formal proofs (e.g. using Coq or Agda)

(FYI that property is in fact false, since it doesn't hold for -2147483648; ScalaCheck's random generators are biased towards such "problematic" values, e.g. -inf, NaN, etc., so it usually find such things)

Re: User settings, Lamport clocks and lightweight formal methods

#22

Post by User23 » Thu, Jul 21, 2022, 1:37 PM UTC

dmitriid wrote: post #17

User23 wrote: post #3

Interesting. Incidentally, I would claim that TDD done properly is in fact a lightweight formal method. It helps to be conversant with some kind of formal semantics, but you can definitely play a bit fast and loose by treating your tests as a lightweight specification. In that case any formal properties I want the code to have that can't practically be expressed in the test is included in a comment on the test. Also,…

> I would claim that TDD done properly "I get paid for code that works, not for tests, so my philosophy is to test as little as possible to reach a given level of confidence" — Kent Beck https://stackoverflow.com/a/153565

Yes, as a consultant Mr. Beck has no concern about code correctness. He only needs it to please the client sufficiently to maintain his reputation. Since users are used to low quality software, that’s a practicable bar to meet just winging it.

And as a seller of programming books, he increases his target audience by excluding the small percentage of mathematically literate programmers and appealing to the majority who find logic intimidating.

Post reply on HN