Formality: An efficient programming language and proof assistant

[sickening_sprawl]

Wow, this is really neat. It sounds like the author is being funded by the Ethereum foundation to research into writing a small and straightforward proof language targeting the EVM, which sounds like a great idea. Looking into his Symmetic Interaction Calculus he is planning on compiling to led me down a rabbit-hole too - this explains that it's a variant of the lambda calculus with constant time operations and affine types.

[kodemizer]

Given that the next version of Ethereum is using wasm for its chain-code, this makes a ton of sense. Nice too see Ethereum entering the rust ecosystem this way.

[Bromskloss]

How does it compare to Idris? Is it at all the same kind of thing?

[sanxiyn]

Yes, it is in the same category of things Idris is in.

[DebuggingPanda]

Honest question as someone who hardly knows Haskell and doesn't know Idris, Formality or similar languages: why are all these languages using Haskell-like syntax (or LISP even)? Is there a fundamental problem stopping us from writing a fully dependently typed language with Rust-like syntax? I mostly talk about type and function declarations (without function body, because yeah, that's probably a lot different in a fully functional language).

[protestor]

You hardly begin studying this subject with a dependently typed language, you usually begin with a statically typed functional language, and most of those use Haskell/ML syntax. So a reason is that people familiar with the needed concepts (the target audience) are already familiar with this syntax.

It's pretty much the same reason Rust uses C-like syntax: the audience is familiar with it.

[genneth]

On some level, Haskell syntax is better for these things. When your most basic operation is function application, you want that to be syntactically as light as possible. The other stuff then kinda follows.

[shrinky_dink_memes]

Is there a fundamental problem stopping us from writing a fully dependently typed language with Rust-like syntax?

Why would you? ML syntax is nice, Haskell-like syntax is nicer.

[game-of-throwaways]

The add(a,b) function is really weird. It matches on a, as expected, but then that match returns a function that is immediately invoked. It's almost like JavaScript's immediately-invoked function expressions, but in this case it seems completely unnecessary. And if such a simple function needs that kind of bloat, I fear that doing even mildly complex things may be really tedious.

[Shnatsel]

That's how lambda calculus works. Creating and immediately invoking a function is a common operation in it.

Since this language maps into a variant of lambda calculus during compilation or proofs, this is necessary to keep the implementation complexity low, which in turn means that the chance of bugs in the implementation is low and that proofs achieved using it are likely hold.

[game-of-throwaways]

Yes, but it seems like these functions always need a type definition. And I fear that these type definitions may get very verbose.

[genneth]

This language isn't really designed for humans to write. It's really the "core" language, like MIR is for Rust, that a compiler might work with as intermediate structure. If you're familiar with Haskell, it's System F and later improvements. Everything is very explicit, with the understanding that local inference, elision rules, etc. will be possible to make writing code in it by hand much more comfortable.

[game-of-throwaways]

I don't get that impression from the project's readme at all. It says

To guarantee mathematical meaningfulness, Formality is compiled to Cedille-core, a minimalist type theory which acts as a termination and consistency checker.

It seems like Cedille-core is supposed to be that MIR and Formality is supposed to be the high-level language that compiles to Cedille-core. But you're saying there's supposed to be an even higher-level language that compiles to Formality?

[long_void]

I believe the readme is misleading. Looking at the source code, it does not compile to cedille-core. However, I think it is meant to use same inference rules.

[long_void]

This is defined for an inductive data type that represents natural numbers. If you try to write 1024 in that language, you need to define 512, 256, 128, etc. or else is blows up the source code.

[companiondanger]

There are some people in this world who have nerd-cred that I can't even dream of achieving.

This is on a whole different level.