{'fraction_non_alphanumeric': 0.021848739495798318, 'fraction_numerical': 0.005042016806722689, 'mean_word_length': 5.549450549450549, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions

Industrial applications of interactive theorem proving dates back to the eighties. Enabling and achieving industrial successes has been an important focus of the ACL2 community. The ARCADE call-for-papers appears to ignore these results and the potential of automated reasoning in industry in the future. We briefly describe the penetration of the ACL2 theorem proving system into the microprocessor industry, list some of milestones achieved, the obstacles standing in the way, and some future research directions.