3 ms·
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only he
by psychoslave 6mo ago
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only heard about lean through HN posts.
- c0balt 6mo agoI don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool. The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation. [0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Big.20news.20from.20Amazon.20Web.20Services.html https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ https://lean-lang.org/ (Cedar)