Plutus, Haskell, Nix, Purescript, Swift/Kotlin. laser-focused on FP: formality, purity, and totality; repulsed by pragmatic, unsafe, “move fast and break things” approaches
AC24 1DE5 AE92 3B37 E584 02BA AAF9 795E 393B 4DA0
- 0 Posts
- 1 Comment
Joined 3 years ago
Cake day: June 17th, 2023
You are not logged in. If you use a Fediverse account that is able to follow users, you can follow this user.
I should make you aware of the fact that hardened, top-to-bottom formally verified OS’s exist. Some even go so far as to harden and formally verify both software and hardware.
https://www.cs.ox.ac.uk/tom.melham/pub/Gao-2021-EFV.pdf
https://github.com/standardsemiconductor/lion
http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
https://www.cs.cornell.edu/courses/cs6410/2013fa/slides/10-verifiable-systems.pdf
https://aerospacelab.onera.fr/sites/w3.onera.fr.aerospacelab/files/AL04-10_0.pdf
https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD12/005.pdf