mojo VS slides

https://github.com/modularml/mojo/blob/main/LICENSE Is this not it?

Interesting, but the intent seems similar to Chris Lattner's new Mojo language which arguably has similar characteristics and is further along in its development.

https://docs.modular.com/mojo/

Mojo is a programming language that combines the performance and control inherent in systems languages like C++ and Rust with the flexibility and simplicity of use typical of dynamic languages like Python. Because of its combination of performance, extensibility, and usability, its design makes it possible to construct high-performance systems, which makes it a good option for AI development.

If you take a look at the optimized Mojo code doing the matrix multiply [1], it takes an expert to understand. It’s not just some simple for-loops in Mojo they’re comparing against.

[1] https://github.com/modularml/mojo/blob/5ce18c47a27c0c4123de1...

Mojo truly unlocks a world of possibilities in high-performance computing.

For a concrete example of Liquid Haskell, see how Gabriella Gonzalez safely removed bound checks of high-performance protocol parsing, in "Scrap your Bounds Checks with Liquid Haskell" [1].

With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. With static types, programmers can write correct programs faster, and the programs also run faster.

As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2].

[1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"

[2]: https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"

> static analysis isn't going to deal with every scenario like access based on inputs.

Not true.

With proper abstraction, static analysis proves the absence of bugs under all relevant inputs, which gives stronger guarantees than testing at development time (which only checks for a number of inputs), and is lighter than runtime checks (without runtime overhead).

An example is the use of a static type system, which eliminates a whole class of bugs under all possible values of the same type (those due to type mismatch: passing an integer into a function expecting a string), which is stronger than a test suite testing certain inputs, and does not have runtime overhead (unlike runtime checks).

Going further than usual type systems, people study refining types by possible values (such as positive integers as a refinement of all integers), and the result is refinement types, which is what Liquid Types is based on. And you can see this in action in the full example [1], such as { n : Int | 0 <= n } which refines n to be a positive integer.

[1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Full program - Scrap your Bounds Checks with Liquid Haskell"

PS: I figured that setting the record strict may benefit others, such as https://news.ycombinator.com/item?id=37380176.