r/ProgrammingLanguages

Disclaimer: I am an experienced developer, not a logician. So what I write here might be full of mistakes. A lot of it comes from chats with different AI bots.

When I say "real" programming I mean programming of real, complex, performing applications, with good tooling. Not necessarily using a popular language, although this might help.

For years I have waiting for a way to use the techniques used in theorem proving for programming. Now it looks like some realistic possibilities are getting closer.

I know there are 2 languages used for theorem proving, Lean and F*, that can also be used for programming.

However, Lean has poor memory management (only reference counting), and F* seems particularly unfriendly and with poor tooling support. But it does have good memory management thanks to Low*.

On the other side, Rust has Verus and Aeneas.
Verus is easier to use, but not as powerful, as it doesn't have dependent types and calculus of construction. It uses SMT, which apparently is less powerful.
Aeneas translates Rust to Lean, Rocq or F*. This makes Aeneas more powerful, but also harder to use, because there is more proof needed. Aeneas is also not yet able to fully translate Rust.

If this is correct, it looks to me that the best way is to use Rust, Aeneas to translate to Lean 4, and use Lean for proofs. So I can have:

• Rust's good memory management, tooling support and performance. Plus the rest of Rust, programming is not only formal verification

• Lean's calculus of constructions, also with some tooling support. Lean has at leas a VSCode plugin

Aeneas can't translate everything yet, but the limitations don't look so bad.

How does that sound?

I'm making a language with an insane type system and I was thinking that combining monads & effects needs to be easier.

I don't fully like monad transformers, effects, polysemy, fused-effects, etc, and lifting anything other than weights. There is so much boilerplate. For example, there is difficulty is that combining monads is order-dependent (some monads don't "commute")

I came up with a simple solution that seems to be just working? So there is || ("or else") operation in my language. Simplified: intersecting with "A || B" tries to intersect with A, and if it's an empty set, it tries to intersect with B. Then it returns the intersected result. Pattern matching is expressed via that operation. And it fits if we expand it to type-level functions as well!

Here we go:

getOdd : Int -> Option Int
checkPositive : Int -> Throw Int

program : Int -> (Throw || Option) Int
program number = x <- getOdd number
                 y <- checkPositive x
                 y + 1

// 5  -> ok 6
// 4  -> none
// 0 -> none
// -1  -> thrown "fail"

It looks really convenient, in my opinion. It also specifies order, so there can be any monad and the result may be dependent on order (but in most cases it's fine). Do you see any errors? I tried Lean-vibe-proofing different parts (extended monad laws, etc), it sounds like it's correct.

Full code example in my lang c(x), it's missing some syntax sugar, but works:

// Option and Throw monads & implementations
Option A = {some (value: A) | none}
Option A : has returnOf value = some value
               bindOf (some value) next = next value
                      none         next = none
Throw A = {ok (value: A) | thrown (message: String)}
Throw A : has returnOf value = ok value
              bindOf (ok value)       next = next value
                     (thrown message) next = thrown message

// ignore, it's Monad implementation, "->" picks these up
return : for [f, a] ((a -> f a) & {returnOf f})
bind (f action) next = bindOf f action next

// action in monad 1
getOdd : Int -> Option Int
getOdd number = if number % 2 = 0
                    none
                else 
                   some number
// action in monad 2
checkPositive : Int -> Throw Int
checkPositive number = if number > 0
                          ok number
                       else 
                          thrown "fail"

// combine monads/type functions easily with or-else
// it maps to every "has" method and only matching bind is selected
program : Int -> (Throw || Option) Int
program number = x <- getOdd number
                 y <- checkPositive x
                 y + 1

x <- read Int
print (show (program x))

Things that might require explanation but are not crucial for understanding:

• has-methods are just generic functions on crack (x : has f = 3 => f x = 3, for this exact x) that also generalize to record field getters

• <- is a not a typical do notation: every bind can have it's return type extended with another monad. Check out "polymonads" for a more general concept around this, but my one is narrower.

• || maps to every has method in the intersection of types with the has method (so (x : has f) || (y : has f) => z : has f = f x || f y)

Why?

Because you can use different simple plain monads in one do block! And because combining semantics of different context is very expressive and readable at the same time!

program : (List || Throw || IO) Int
program =
    a <- read Int   // action in IO
    x <- [1, 2, a]  // action in List ("non-determinism")
    validate x      // action in Throw
    x

All of that is statically typed and compiled btw. I'm exploring refinement + gradual + dependent types with a couple of extra ideas and it absolutely nuts (follow me on , I'm going to publish the updated language soon, the current public repo is 10-year old and not very correct)