Post #4215123

@agl@infosec.exchange > I think we haven’t really explored this in normal contexts. Indeed, there are actually "dozens" of us who want to, and are exploring, how to bring this interesting paradigm to others. As well as exploring what this paradigm gives us in the first place.. > I feel that the overhead of these languages previously precluded their use in all but specialised domains. Now that the overhead is much less, I think it’s an interesting avenue to explore. But certainly not a guaranteed success. Indeed! If you are not familiar with it already, you should explore: https://hacspec.org/ It shows one way of doing things. There are, however, other dependently typed languages (Agda/Idris2) which provide a different view (compared to Roq/Lean) of working with the machine to build verified software.