Cool!
Maybe I’m misunderstanding, but how is this related to Nix?
There’s a non-coincidental overlap of interests among people who are into Nix, functional programming, or formal methods. As a Nixer, I enjoyed reading the post and know a few people around here who likely would, too.
Very interesting article. As pointed out in the article, I too think that the future is bright with regards to formal methods. With the increasing focus on security, due to the possibility of AI discovering every small flaw in a program and being able to exploit, I think that a formally verified program will be worth more tomorrow than it was yesterday.
It could be cool if us Computer Scientists could be hired to do formal methods and verifications rather than writing code all day long.