Lambda Days 2020: Day 2

Lambda Days 2020, summary of second day. Don’t forget to read the wrap-up of the first day before this one!

Keynote: Proving Algebraic Laws in Scala using Stainless and System FR by Viktor Kunčak

Opening the second day, the keynote by Viktor was an introduction to Stainless, a formal verification tool for Scala. He started with an interesting question regarding property based testing: “when should it stop?”, meaning, how many checks are necessary? One hundred? One thousand?

Stainless generates formulas that imply correctness

Quoting Stainless website: “Thanks to its use of formal proofs, Stainless can establish safety and termination properties using symbolic reasoning, covering infinitely many inputs in a single run of verification”. This tool has the same sort of fundaments that attracted me to use Quill (proper theory behind it). I strongly recommend everyone to check it out!

At the end, Viktor invited the community to contribute to the project or even start porting it to Haskell or Clojure!

The power of Π by Thorsten Altenkirch

In his talk, Thorsten delivered a lesson about Dependent Types, and the fact that Haskell type system lacks it (I didn’t know that). He presented some of the use cases for dependent types:

• Types to all sensible programs
• Schemes as part of the data
• Eliminating runtime errors
• Capturing gradual typing

It works as a big product. An infinite product

After that, Thorsten discussed myths and facts about dependent types:

Myths:

• Programming in DTP languages is more difficult
• You have to prove that your program is terminating
• DTP languages are not Turing complete
• DTP doesn’t work with effects

Facts:

• DTP makes big demands on the IDE
• Compile time can be an issue
• More precise types can hamper reusability
• DTP toolchais are not yet ready for professional developers

A strong static type discipline requires dependent types

A Family of λ-Calculi with Ports by Seyed Hossein Haeri and Peter Van Roy

This talk was actually delivered just by Seyed, and according to his slides, it had a different name: Piecewise Relative Observational Purity, A New Paradigm for Distributed Systems Programming.

Seyed started with a parallel between systems architecture and functional programming, discussing the good parts and the bad ones, and the fact that side effects are inherent part of distributed systems, therefore it’s necessary to give up purity… or maybe not!

His reserch named A Family of λ-Calculi with Ports is a possible solution to the problem. Using a client-server model as example, he walked us through the main topics of the research.

Purity is relative. Depends on who is watching

The paper is a very interesting read.

Automated Reification of Source Annotations for Monadic EDSLs by Agustín Mista

Agustín presented a tool that automaticaly reify source annotations in Haskell. With such tool, it is possible to solve problems like name binding and error reporting.

That’s all I can say about the talk, my knowledge of Haskell was enough just to understand the problem that Agustín is trying to solve :)

Elixir vs Scala by Ludwik Bukowski and Kacper Mentel

This was a very practical session. A comparison between Scala and Elixir, given a specific problem: recognize a digit in drawings. They did it using the k-nearest neighbors algorithm, using the distance as comparison metric.

Writing native implementation is not that hard

After defining the specifications of their environment, the first solution was with vanilla Scala and Elixir. Ludwik and Kacper shared the results and Scala was faster.

Then they started tuning up Elixir, first with Porst and the second attempt with NIF, which significantly improved the performance of the Elixir solution. In order to take Scala to the same level, they implemented a solution with Java Native Interface (JNI) as well. After tuning, Scala was more performatic again.

Using native solutions can be performatic, but risky. It was nice to see the results they achieved, and the well defined way specified to compare both solutions.

Enhancing the type system with Refined Types by Juliano Alves

I was there, but didn’t exactly watch the talk. I’ve heard it was awesome though ;)

Slides available here

Privilege as a technical debt by Amr Abdelwahab

Amr brought up a very relevant topic nowdays: how little we acknowledge our own privileges - which is actually hard to realize by ourselves. Telling us about his own personal journey to learn about privilege, Amr delivered a very strong message.

I realized that my whole life I’ve been lacking context

The wiki definition about provilege is wrong, the topic is much deeper

Amr mentioned places where people cannot express themselves, or even confess their love to other people. He listed many provileges we commonly don’t even think about, and how they influence the world around us. Some famous examples are the racist camera and the sexist airbag.

Once speaking to engineers, he made an interesting allegory with technical debt: Humanity is the project that we are all maintaining. We have to move forward, but be mindful.

Being a software engineer is in its own a privilege

Amr suggested we all should try an empathy exercise, thinking about what we can do as an employee, as a company, as a community member, etc. I believe every software conference should have a talk like this one.

Keynote: How to let kids outsmart you and why they should? by Van Anh Dam

The final keynote was delivered by an educator. Van Ahn Dam discussed the importance of education and how we all can help to provide it - developers can do a lot to support it.

Work will keep changing, so the skills in demand will follow. The development of technical, soft and social skills will be vital to communicate effectively with people and machines to solve complex problems.

When it comes to education, digital resources are still limited. Some of the current challenges are:

• Lack of resources
• Lack of teachers and role models
• Lack of growth mindset

Van discussed what makes an ideal environment for education, presenting principles and tolls she has been using. After that, she showed the video about one of her projects, a brilliant initiative to conciliate the dedication of grandparents with education of their grandsons, called Very Senior Developers:

At the end, she invited us all to colaborate. One way to find opportunities is CodeWeek.

Everyone needs to get involved and take responsibility in building future

Last but not least, we had a special guest. One of Van’s student closed the keynote with a few words about her learning journey, starting to learn coding from scratch when she was 8, and what she can do now at the age of 11.

It was a great way to close the event. Thank you Lambda Days for such a great conference. I hope I will be with you again next year!