4 ms·
Guess what one of most field-proven verification tools uses and verifies? LISP via ACL2. The dialect of lisp that ACL2 verifies is not very powerful at all.
by kd0amg 11y ago
Guess what one of most field-proven verification tools uses and verifies? LISP via ACL2.
The dialect of lisp that ACL2 verifies is not very powerful at all.
- nickpsecurity 11y agoIt can be integrated into LISP or transformed into forms of Turing complete languages. It doesn't have to be powerful to be used powerfully. :) Part of my recurring them that you can have both worlds.
- kd0amg 11y agoAny language's code can be integrated or transformed into some Turing-complete language. That doesn't make a language powerful. You don't see anyone raving about how amazing the language of variable-free arithmetic expressions is, but that's already integrated into most languages people would call "powerful." The idea that ACL2 verifies a powerful language is outright false. ACL2's verified language is stripped down (no first-class functions, nontermination, exceptions, etc.) because added power makes it too hard to verify.
- nickpsecurity 11y agoAlright I'll give you that. My main argument is for a language powerful enough for both solving problems concisely and creating DSL's should be used with DSL's for common or hard problems. The DSL's or the language can be subject to verification.