3 ms·
If you really want to build on "rock", check out Bedrock: http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ . Don't just prove your program i
by jeremysalwen 9y ago
If you really want to build on "rock", check out Bedrock: http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ . Don't just prove your program is memory safe, prove it satisfies arbitrary properties! (A bit tongue in cheek, but the tools are really cool). Check out http://adam.chlipala.net/cpdt/cpdt.pdf http://adam.chlipala.net/cpdt/cpdt.pdf for a nice introduction.
- bpicolo 9y agoVery formal sorts of languages are super interesting. They might tend towards striking the wrong balance, though. Rust is super interesting to me because it prevents the most common vulnerabilities w/regards to memory safety that show up time and again, but it's accessible enough that it's got a big community and a ton of high quality libraries. I think that's a pretty awesomely potent combination.
- bjz_ 9y agoFor the short term and mid term yes. However I do hope that in the long term the ideas from ATS, Liquid Haskell, Idris, F*, etc. will be iterated on in order to make them more accessible and usable. In the mean time we'll probably start to see Rust graft on more and more correctness tools like dependent types and SMT solvers, and it will begin to get a little ungainly, like dependently typed Haskell is. But there's only so many ideas you can try out in a new language, and Rust has made the right decisions on that front in the interests of getting into production this decade. :)
- harveywi 9y agoI would love to see an experience report of someone who has used Bedrock in a nontrivial application.