54 ms·

fyi Dafny is written by Microsoft and used by Amazon: https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing https

fyi Dafny is written by Microsoft and used by Amazon: https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing https://www.amazon.science/blog/how-we-built-cedar-with-auto...

mintplant 2y ago
Recently replaced by Lean, though. At least in Cedar. https://github.com/cedar-policy/cedar-spec https://github.com/cedar-policy/cedar-spec https://lean-lang.org https://lean-lang.org
- pjmlp 2y ago
  Which is also a Microsoft created language, https://en.wikipedia.org/wiki/Lean_(proof_assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant)
  - mintplant 2y ago
    Yes, Microsoft Research is huge in this space. Z3, Boogie, Corral, Dafny, F*, Lean...
    - naasking 2y ago
      F* seemed promising at one point, but haven't heard much about it in a long time, what happened to it?
- ComputerGuru 2y ago
  Thanks for that. Any idea why? Couldn't find anything by searching their github repo.