We’ve been using data-types as well, especially

Either

for proper modeling not only the result but the errors as well. Haven’t gotten to

IO

and such yet 🙂 Folks seem to like it, although there are some complaints that they have to now always deal with the ‘left’/error case… which is good, better than just swallowing an exception 🙂

I'm likely going to do a training round with Scala & cats/cats-effect just to introduce concepts on a stable codebase, but we're committed to Kotlin as the next language. I'll likely introduce Arrow once it has stabilized and it should be easier since most or all of the cats/cats-effect concepts should just translate

data type are ok for most people. the problem that I'm facing now and it seems hard to overcome is "Rx/Coroutines vs IO"

actually is more of rx/coroutines + IO 😄

and the room goes cold very quickly

@ivanmorgillo The answer to that question is to respond with "Show me a real-world mobile startup problem that everyone has that I can only solve with Java/Kotlin/Swift instead of assembly"

because FP + developer discipline yields benefits in maintainability and extensibility down the road instead of immediately.

The most immediate benefit is being able to prove that the code works generally instead of just demonstrating the code works for specific cases

The former can be demonstrated using property-based testing (commonly available) or formalized proof systems (available in more advanced languages); the latter is common in most unit tests

Immutability yields testability using property-based testing as well. It is difficult or impossible to prove anything about a system with more than one thread sharing mutable state

Formal methods are soon going to be available for Kotlin. We are working on it.

and automatic discovery of safety and satisfiability of pre post conditions for unsafe apis that will question the value of an FP program compared to a regular oop imperative one.

Since we will be able to determine if they are safe

regardless of style

@Bob Glamm http://logicrunch.it.uu.se:4096/~wv/eldarica/?ex=threads%2FtwoThreads-unsafe

@raulraja if I'm reading that correctly it sounds like effect-safety will be enforceable at the compiler level with plugins? That is, we'll be able to start within

IO

in main?

it’s actually quite possible and happening in Kotlin too

Sure, for simple cases something like that or TLA+ can validate the state changes and the model

@Bob Glamm No, Simon is gonna take you there to suspend, and others in 47 are gonna show you the code you are writting that is unsafe as you type it

and will generate counterprograms and tests

I know Amazon validated some of their concurrency with TLA+

and if it works how I have envisioned it will remove the need for property test and perhaps most testing in general

Also the false elitist notion that someone new to Kotlin can’t write a correct program without knowing all the warts of the lang and Java and to do that that you need seniority

What we are gonna be using is more powerful than a compiler and will dependently analyze all the unsafe code in the editor and at compile time

It will also allow you to extend the rule set with new logical axioms you can write quantified polymorphically as prelude of what your library or system rectracts or adds as “safe”

also is not just for Kotlin. Frameworks, libraries and other langs too

Ok, when I read "safety" I read "pure functions to the edge of the world" - is that what you are referring to?

safety is totality

oh total functions, ok

the guaranteed that your program has all paths covered