The rapid development of machine learning (ML) enables practical applications including in smart contract development. As a superior smart contract language, Juvix can provide extra support using ML in the following fronts:
- Generate correctness proofs
See this paper. When combining the mechanics of Proverbot9001, CoqHammer and CoqGym, a meaningful portion (28%) of the correctness proofs of CompCert (written in Coq) was generated. Note that the difficulties of the generated proofs are evenly distributed - i.e., it is not only generating proofs that are trivial for users to write.
Juvix is built with the intent that smart contracts written in it are more secure because users can write proofs to prove important properties of a contract. However, writing proofs is a tedious and costly task. Juvix would be much more attractive if it can write a significant portion of the proofs for the users.
- Detect bugs (static analysis)
Bugs in smart contracts can be very costly. Static analysis tools that help users catch bugs are therefore beneficial.
Although the majority of important properties of a smart contract should be proven correct, a static analysis tool for Juvix is still worth considering. First, without such a tool the users may be spending time trying to write proofs without knowing that there is no proof because the code is buggy. A static analysis tool can assist users in spotting bugs before they write their proofs. Second, users who don't want to spend time to write proofs can still use the tool which helps them catch bugs.
Traditional static analysis tools without learning have existed for decades. However, there are limitations on what they can do. Another problem is the pervalence of false positives, which is often a pain point for developers. Recent ML research (e.g., see Hoppity) alleivates some of these problems. It is therefore worthwhile to consider developing a static analysis tool for Juvix using both traditional techniques along with recent ML techniques.
- Search for vulnerability
Using graph neural networks, one can transform smart contracts semantics to graphs (see this paper). Then one can perform graph level analysis to perform various analysis, including detecting vulnerability.
See also Machine Learning Model for Smart Contracts Security Analysis and SoliAudit: Smart Contract Vulnerability Assessment Based on Machine Learning and Fuzz Testing. Both use ML to detect contract vulnerability in Solidarity. The same methodology can be applied elsewhere.
- Improve user experience with improved type error feedback
See this paper. Having helpful error messages is one of the most important features users care about. Using
To add the proposed features above, one of the most important challenges is to provide training data for supervised learning. The larger the training set, the better the AI will perform.
Coq is the most widely use proof assistant thus far. It has by far the largest code base on proofs. Many of the projects mentioned above use Coq codes as training sets. If Juvix has syntax similar to Coq's, this challenge is solved for the most part.
Having syntax similar to the most widely use proof assistant also has the benefit of decreasing developer overheads. Programmers who know Coq can comfortably code in Juvix. Of course, Juvix has the addition feature of usage tracking, and syntax for that would be added because Coq doesn't have this feature.
Although there are plenty of research supporting the above features, to fill the gap between the research and application to Juvix is not a trival task. I recommend we re-visit the research once Juvix is more mature.
We are in a field that is constantly evolving and very competitive. To stay ahead, Juvix cannot afford to dismiss the recent advancements of ML applied in programming languages. On the other hand, adding these practical and irresistable features would further secure Juvix's future place as the leading smart contract language.
Inspired by the following talks of the MAPL track of PLDI 2020:
- Hoppity: Learning Graph Transformations to Detect and Fix Bugs in Programs
- A Gentle Tutorial on Graph Neural Networks and Its Application to Programming Languages
- Generating Correctness Proofs with Neural Networks
And the following papers from the research papers presented at PLDI 2020:
- Type Error Feedback via Analytic Program Repair