Design

The philosophy of Juvix is one of generality and flexibility. It should not be the case that the Juvix compiler developers should have many extra tools over the users of the language. The compiler/language developers/designers should be able to chose what is canonical, however the forms of the language should be generic in a way that ordinary users could have made if they so wish.

For example, the form of def in the frontend language, is not a fixed piece of syntax, but rather a simple macro over a primitive that is most suitable for our core type theory. This means that if one is an application developer for some domain, like web-browsers, they can make their own version of def (def-command) that fits into their domain better (registering hooks and functions into the web-browser itself!).

In order to achieve this goal of flexibility, Juvix has made many design decisions that allow traditionally built in tools to be first class in Juvix.

• Some of the major design decisions

  1. Small core syntax

     • This means our syntax isn't special

  2. Image based system

     • This means Juvix can talk about the environment in which it lives in.

• Some Applications that are traditionally built in or hard to achieve without these systems

  1. Build tools can be made in the language!

  2. Live documentation tools can be made while developing!

  3. Proof Assistant with more power to effect the environment for a better interactive experience.

  4. Better proof generation and tools to introspect various aspects of their Code.

Another design goal of Juvix is to allow for safer programs that are mission critical. When one is writing smart contracts that have millions of dollars at stake, a mistake is unacceptable. Thus Juvix has dependent types. Dependent types are wonderful at removing entire classes of errors with proofs about behavior. Further they can make many idioms in a typed language simpler.

However dependent types on their own can be confusing, as the specific incantations one needs to write to be able to effectively prove code is often not intuitive. Juvix thus seeks to make tooling in this area better, offering abstractions that help the language work to help you achieve your goals.