bodzioney

5 ms·

1. 1.▲
   by bodzioney 3mo ago

   Interactive theorem provers are what verifies (or proves) the proof here. This means you don’t even have to look at the actual proof to check its correctness. You just have to make sure the theorem definition is what you wanted (not to say
2. 2.▲
   by bodzioney 3mo ago

   To brew? Sort of. I use nix-darwin for everything. However, some things don’t play nice with nix. In that case you can use nix-darwin to manage brew. Basically you give it all the packages you want, and it generates a brew file and uses it.
3. 3.▲
   by bodzioney 1y ago

   Yes exactly. Aarhus had Martin-Löf, Nygaard, etc. Similarly, INRIA has had many influential researchers as well as OCaml and Rocq. Talent (and exciting projects) attracts more talent. But that doesn’t mean it doesn’t exist in US. Penn, Corn
4. 4.▲
   A Brainfuck interpreter written in Rust(github.com)

   2 points by bodzioney 3y ago|1 comments
5. 5.▲
   by bodzioney 3y ago

   I was inspired by the recent Brainfuck posts, and decided this would be a good time to practice Rust.