Announcing the New Athena Language Website
We’re excited to announce the official launch of the Athena language website. Alongside the website, we’ve also built the Athena playground so you can try Athena directly within your browser. IDE support is available as well via the implementation of the Language Server Protocol (LSP) support for Athena.
LSP-based IDE support for Athena is available to install in Visual Studio Code on the extension marketplace (you can also search for it within VSCode and install it with a single click). The source code for the language server is open sourced on GitHub. Special thanks to Nathan Whitaker for all of his work on the LSP implementation.
IDE support, at the time of writing, primarily provides syntax highlighting and friendly error messages. A prototypical implementation of code navigation via goto definitions is disabled by default, but can be enabled in the extension’s settings page within VSCode. This feature is known to be a bit buggy, but will stabilize in the future. Beyond goto definitions, our plans for the LSP include implementation of:
- Displayed information on hover, such as documentation & type information.
- Support for context-aware autocompletion.
- A pausable debugger to inspect and change the context & state during proof execution.
- The ability to display the available methods, functions and theorems provided by an imported module.
If you have other features you’d like to see, or if you encounter unexpected behaviors within the VSCode extension, we invite you to file a GitHub issue or even contribute, yourself!
The playground includes a number of examples that showcase many of Athena’s interesting features, including equational reasoning, proof chaining, proofs in both propositional and first order logic, automated theorem proving, SAT solving and SMT solving. The playground also comes with a scratchpad.ath file which contains an empty module you’re free to modify in any way (you can also modify any of the examples to play around with them, too, of course). The syntax highlighting within the playground is not quite as robust as that of the VSCode extension. We have many plans toimprove & expand the playground’s capabilities and robustness as well.
To learn Athena, we’ve curated multiple learning paths depending on the time you have available and the depth to which you want to explore Athena’s capabilities. The full set of tutorials as well as a guide on which tutorials to follow and in which order are located on the Learn page of the website. The material should be more than enough to develop proficiency in Athena. An even more comprehensive documentation site is also currently under construction.
We are still actively developing tools and documentation to facilitate Athena’s increased adoption. Further, R&D into software verification and systems modeling with the use of Athena at various professional organizations has recently begun. The project domains range from embedded systems to peer-to-peer networking and distributed consensus. We are excited to share updates about these projects in the near future.
For installation instructions, please visit the Proof Engineering blog post, “How to Install Athena”.
In the near future, we will also be releasing a user forum where students, professionals and researchers can post questions, share work, and discuss Athena’s use & development. So, stay tuned for that as well.
Finally, we invite you to check out the Athena Foundation’s GitHub organization, browse the repositories and be sure to open an issue if you note any bugs or areas of improvement!