Sponsorship

Lustre

Find Amazon overwhelming? This AI-powered shopping tool called Lustre does extensive product research for you—from reviews to prices—so you can always get the best product for your money. Check out Lustre here. It’s 100% free!

Not subscribed to Console? Subscribe now to get a list of new open-source projects curated by an Amazon engineer in your email every week.

Already subscribed? Refer 10 friends to Console and we’ll donate $100 to an open-source project of your choice!

Share Console

Projects

AttackSurfaceAnalyzer

Attack Surface Analyzer is a Microsoft developed open source security tool that analyzes the attack surface of a target system and reports on potential security vulnerabilities introduced during the installation of software or system misconfiguration.

language: C#, stars: 2107, watchers: 65, forks: 220, issues: 36

last commit: August 04, 2021, first commit: February 15, 2019

https://twitter.com/OpenAtMicrosoft

Kind

Kind is a minimal, efficient and practical proof and programming language.

language: Kind, stars: 1950, watchers: 70, forks: 79, issues: 23

last commit: September 03, 2021, first commit: February 19, 2021

http://uwu.tech/

drago

Drago allows you to securely connect anything with WireGuard and manage all your networks from a single place.

language: Go, stars: 687, watchers: 24, forks: 26, issues: 21

last commit: August 18, 2021, first commit: January 08, 2020

https://www.seashell.sh/

clockwise

Clockwise is a meeting cost calculator designed to encourage more efficient meetings.

language: Go, stars: 434, watchers: 11, forks: 6, issues: 7

last commit: August 08, 2021, first commit: July 27, 2021

https://www.linkedin.com/in/alexander-perlman-a396a654/

Console is powered by donations. We use your funds to grow the newsletter via advertisement. If you’d like to see the newsletter reach more people, or would just like to show your appreciation for the projects featured in the newsletter, please consider a donation 😊

Donate Today

An Interview With Rígille Menezes of Kind

Hey Rígille! Thanks for joining us! Let’s start with your background. Where have you worked in the past, where are you from, how did you learn how to program, and what languages or frameworks do you like?

I’m a math student from Brazil. I learned python when I was young but I only really invested in learning programming after getting discouraged by the prospects of academic career. I got a job as a C++ developer in a startup that was building a trading platform. Most of my general programming experience comes from my year there. Now I’m working at uwu tech. My favorite languages are C and Kind.

What about an academic career discouraged you?

Academic work seems very restrictive for me. Industry has its restrictions too, but I see them as rooted in the demands of the public. Those demands act as a standard and objective criteria of success. Academia on the other hand feels more disconnected and subjective.

How did you find out about uwu tech and what made you decide to join?

I found out about uwu tech because of a friend of mine, Vitor Chiarelli, who was from my class. He told me it was a company devoted to developing applications with that new proof language. Looking back it was such a coincidence. I had become interested in formal methods after reading “How to write a 21st century proof” by Leslie Lamport not long before that. At the time, I was addicted to the “Software Foundations” series, but I hadn’t told him about that. Sometimes things just work out.

What is one app on your phone that you can’t live without that you think others should know about?

MessagEase, for sure. It's a keyboard app. Qwerty wasn't designed to be so small and because of that people are slow to type and make mistakes. The most popular solution, kind of crazy if you think about it, is to make a program monitor and guess what you meant to type. Why not design a keyboard that doesn't need to be big? That's MessagEase. The transition took me one week years ago. Now I can type fast, correctly, without looking, and even use vim on my phone easily :)

If you could teach every 12 year old in the world one thing, what would it be and why?

Lojban of course!

Just kidding. I wouldn’t really make every 12 year old learn something. No single teaching could fit everyone’s contexts and preferences, even more so considering that learning something makes you incur an opportunity cost that might be too big. That said, non-violent communication is something I could teach that’s most likely to be useful in general.

What are you currently learning?

I'm mostly learning and researching about compilers on the side, working through Andrew Appel's books. I think Kind could one day be one of the fastest languages out there but it's necessary to target a lower level language to one day seize this potential. My reasoning is that more optimizations become possible when the compiler knows more about the behavior of the program. Most compilers have to guess what the program is about, but not Kind's. The user could tell us anything he wants about his program using the type system.

Also some mathematically inclined people showed up in the community and they want to implement real numbers in Kind. I'm researching existing implementations to give them guidance.

Do you have an order you recommend people read Andrew’s books in?

To learn about compilers I recommend starting with “Modern compiler implementation in ML”, there are also C and Java versions to choose from. “Compiling with continuations” talks about a way of representing control flow that’s especially useful for functional language compilation. To learn about formal methods I recommend the “Software foundations” series and then “Program logics for certified compilers” if you’re feeling brave.

How do you separate good project ideas from bad ones?

The best way is to try them out and see how it goes. Try to realize as soon as possible if it's bad, if it is, drop it. I'm still getting used to this, and still impressed by how easily Victor throws away bad projects. Everything looked very different one year ago, now it's much better.

I also believe you can find out which projects are bad faster if you first develop and reason about a specification be it formal or informal. What's the state of the system? How does the state change? What are the invariants? Those questions direct you to the most important aspects of your project, even if it has nothing to do with software development.

Who, or what was the biggest inspiration for Kind?

Well I can't speak for Victor here, but Kind is only possible because Aaron Stump and Peng Fu developed the theory of self types in 2014.
The link to the original paper is this one. I must admit I have a hard time reading it. Even though I learned how to program in some dependently typed languages I don’t have a type theory background and it isn’t easy to search for the meaning of a notation. What works surprisingly well is to start at the examples and go back from there.

Are there any overarching goals of Kind that drive design or implementation?

Yes there are exactly two goals: keep the implementation simple and make developers more productive. All other aspects originate from these goals.

It's hard to be as expressive as a mathematician would like and keep a simple implementation. The things you can define using set theory are wild. Maybe too wild. You might have heard Banach and Tarski proved you can divide a sphere in disjoint parts and rebuild them as two identical spheres without ever stretching anything. And they really proved it. The argument is sound and the logic is consistent as far as we know. But if I presented to you a point of the sphere, could you calculate whether it goes on the first sphere or on the second sphere? You can't! There's no such algorithm. So is this even real? I don't know… Anyway we would like to make Kind's logic more expressive to better serve e.g. mathematicians but we don't know how to do that yet.

Also to make the language easy to use we allowed programmers to write infinite loops. That means circular arguments are also accepted by default. Checking that your argument isn't circular and that your program terminates will be optional.

What is the most challenging problem that’s been solved in Kind, so far?

I wasn't around when it was done. But from a purely technical perspective the type checker for the core of the language was the most challenging problem. It's just 700 lines of Javascript but it took many months of research, trial, and error to get there.

From a more human perspective the biggest challenge was to package all this in a way that’s useful and friendly for everyone. I’ve been leaning more of the technical and theoretical aspects here because I find it all really interesting. But you don’t need to know any of this to use Kind. Indeed at uwu tech, about 6 months ago, 5 people with little or no programming experience were hired. After 3 months they were already building a multiplayer game with rollback netcode, reactive user interface, and calculating state from a stream of events.

I could teach Kind to my non-programmer friends and it would be one of the fastest ways to build these kinds of web apps, that’s beautiful. We still need better documentation though.

What is your typical approach to debugging issues filed in the Kind repo?

First I try to reproduce the error with the smallest example possible and then debug using logs. Since functions are pure by default you can narrow down the undesired behavior looking at what parameters were different when something went wrong.

How is Kind intended to eventually be monetized?

A programming language is hard to monetize. What you can do is to build a product with that language and monetize that. I mentioned uwu tech, it’s a company created by Victor — who’s the one that actually started Kind much earlier — that’s building products using Kind. We’re currently building games and doing some cryptocurrency-related work.

There’s also an idea floating around to create a trustless market for theorems and programs. Imagine you could write a unit test, attach some money to a smart contract and get a program. You wouldn’t need to review the program for correctness because it would be proven to pass your test in all cases. We have most components needed for that, we just don’t know how to split the reward among many contributors in a way that incentivizes everyone to share their code freely. A winner-take-all model would incentivize people to withhold their partial results.

Can you say more about the cryptocurrency project?

Unfortunately I can’t give more details about the kind of cryptocurrency work we’re doing yet. But it shouldn’t be long before it becomes public.

How do you balance your work on open-source with your day job and other responsibilities?

I’m currently working on Kind full-time :D

I also have to worry about college and taking care of my kitty, but there’s plenty of time for that if I stick to a routine.

What is the best way for a new developer to contribute to Kind?

Chat with us at telegram, ask questions and share your ideas :)