Why

Experiments with data structures and algorithms implemented in FP using Erlang.

I am exploring how development focusing on the correctness and reliability looks like, based on my experience in Scala, Haskell and formal verification in Agda and Rocq:

• property tests, inspired by formal verification e.g. https://softwarefoundations.cis.upenn.edu/vfa-current/index.html
• use spec/types
• use of static code analysis
• unit tests

What

• binary search trees src/bst.erl, test/prop_bst.erl
• red black trees red_black_tree.erl, test/prop_red_black_tree.erl

How Rebar3

• new property test (property names - , file - test/prop_XYZ.erl)

rebar3 new proper red_black_tree

• run PropErty tests

rebar3 proper
rebar3 proper -m prop_bst

• re-run property compilation / property tests on file change

find . -name '*.erl' | entr rebar3 compile
find . -name '*.erl' | entr rebar3 proper -m prop_red_black_tree

• static code analysis using Dialyzer

rebar3 dialyzer

• cross file analyse using xref:

rebar3 xref

• generate documentation (EDoc)

rebar3 compile

• compile

rebar3 compile

• run EUnit tests

rebar3 eunit
rebar3 eunit --module=fib_tests

Erlang and Nix

Nix Shell with Erlang 28

nix-shell -p erlang_28