Alcides Fonseca

Today I gave a tutorial on the Lean programming language and its use for theorem proving. This presentation has an interesting background and I am interested in improving it.

I have known about interactive theorem provers for a while, and during the past couple of years I have taught a course where we ask students to prove properties by hand. Since then, I have been trying tutorials, watching talks and I couldn’t get into any of the different languages: Agda, Idris and Coq.

The main issue is that people who give 50-minute talks about it already know everything about it and can’t really see the issue from the eyes of an ignorant. In particular, ignorants regarding mathematics. Even watching and reading Philip Wadler’s Propositions as Types excellent talk and articles.

Since i’m a frequent z3 user, I’ve heard about the Lean theorem prover (and language) but I really didn’t pay much attention, until I had some free time (actually a deadline for a boring task) and tried the Natural Number Game (NNG) and it blew my mind.

NNG presents theorem proving as a game, in which by completing a level, you learn new tools (lemmas and tactics) that you can use in the next levels. If feels like a puzzle!

Sokoban is a great example that can be compared with this game. If you would try all possible combinations of movements, you would solve any level in an unlimited time. But by looking at the screen, you use your pattern recognition skills to try alternatives that are more probable to solve the level, using a bit of backtracking if you make a wrong decision. Sudoku is a similar game.

NNG takes the same approach, but the Goal window of lean (that shows context and goals) as the game viewport. You see the current scenario (in local variables) and the direction where you want to go (on the goals). You can then make movements (using tactics) that hopefully move you towards your goal. If it doesn’t, you can go back and delete some code.

What NNG lacks is a small explanation of the basic syntax and tactics. Luckily, the Lean window is interactive and you can move your cursor around and learn by moving around the proof. In a sense, it’s similar to the Fog of War in RTS games.

After finishing NNG, I tried to write some useful proofs for work, but I ended up spending 90% of the time reading the lean source code to understand what is available to me. Only after a while I learnt about mathlib and library_search. But even having a productive lemma searcher, I need to understand what tactics I can use to manipulate my context in order to advance towards something I have in hand. This is still a lot of effort to me, and the official documentation (both lean’s and mathlib) requires much more examples and explanations for newbies.

With the goal of trying to get more people to use Lean (and help me!), I gave a tutorial for a mixed audience ranging from undergraduates to full professors. I felt I was the right person to give this tutorial because I know almost nothing about theorem proving and Lean in particular. I showed just the basic steps and left some notes for attendees to make their own path afterwards.

I have made the materials available, including a written version of the tutorial, including exercises and solutions. Feel free to follow them and provide me feedback.

Lean supports several idioms and it is one of the biggest barriers to entering this world. Python’s motto of “one obvious way to write it” that doesn’t even apply to Python would help novices here. Reading the standard library is quite hard because it is written in a “difficult” style that makes use of monads and utf-8 characters. It makes it easier for mathematicians that understand what they are doing, but makes it very hard for non-mathematicians looking for a tactic or lemma that is missing in their proof.

I present Lean as being three different languages: the one for executing code, the one for logic and proofs, and the tactic language (meta). I understand they all boil down to being the same language, but for the user, they are used in different contexts.

I know that you can define a lemma or theorem using def, but that makes it hard for novices to understand what code will execute and what code is used just for proofs. I present proofs in begin-end blocks, showing a procedimental style that mimics the one we use in paper. I understand that they all can be written using lambdas and monads, but that is code quite hard to understand.

This style was the one that clicked for me and I wrote the tutorial to help hackers that can learn by example and have no strong mathematical foundations other can proofs by induction and a bit of Haskell understanding.

Why try to figure it out using logic, when you make your computer use logic for you?

Next one:

I am an avid fan of boardgames. Spending most of my day in front of a computer screen, I enjoy the social fun of being around a table, getting my ass whooped at any random game.

Given the current imprisonment status, I have resorted to skype/zoom together with online platforms (which I have used for years for remote 2-player games. While some online platforms automate several actions, most are less intuitive than their physical counterpart.

Board Game Platforms

• BoardGameArena — one of the best platforms, which some games requiring you to be a premium to open a table (not necessarily play). Usually overpopulated. Free titles I suggest: 6nimt, StoneAge, Takenoko, Jaipur, Tzolkin, Keyflower, Quantum, The Palaces of Carrara,
• Yucata — similar platform. Free to play in two simultaneous game. The UI quality depends on the game itself. Games I recommend: Carson City, El Grande, Glen More, Jaipur, Kashgar, Machi Koro, Navegador, Pompeii, Port Royal, Snowdonia, StoneAge, The Castles of Burgundy, The Voyages of Marco Polo
• BoardgameCore For “real” gamers. I would recommend Antiquity.
• SlothNinja Few deep games. I have only played Tammany hall
• BoardSpace Mostly abstract games, but has some euros like Containers and Medina
• SpielByWeb has Bus, Hacienda, Reef Encouter, Santiago, Tikal and Wallenstein.
• BrettspielWelt Really weird interface, with a lot of non-translated german.
• Boiteajeux While BrettspielWelt is the german boardgame platform, Boiteajeux is the french counterpart.
• Tabletopia, 3D. — Very “manual” in the sense that you have to move cards online.
• Table Top Simulator, 3D win/mac/linux and VR — similar to the previous one, but requires software install.

A mudança recente (e forçada) para ensino à distância mostra-nos as grandes dificuldades que é o ensino à distância. Antes de mais, a maior parte dos professores não estava pronto para esta mudança e as soluções têm sido mais resultado do desenrasque português do que algo realmente planeado. Vou-me focar no ensino superior que é a realidade que conheço melhor (é onde leciono) e é aquela onde os alunos são mais independentes para fazer o seu estudo.

Um dos problemas actuais é que, apesar de várias universidades já assumirem oficialmente que o semestre vai ser todo remoto, não sabem ainda se a época de exames vai ser presencial ou não. Em várias universidades estão a ser estudadas alternativas de avaliação, que vou analisar mais em baixo.

Para começar, estou a estudar duas alternativas diferentes nas duas cadeiras de que sou regente. Numa (com 15 alunos) estou a dar a aula em directo (usando o Zoom) e na outra (com ~180 alunos) gravo vídeos de antemão, que lanço na hora da aula. Os alunos podem ver na hora ou mais tarde. As aulas práticas destes últimos são dados em forma directa (recorrendo ao Zoom).

E a verdade é que para alguém que já trabalhou de forma remote durante vários anos e para várias empresas, eu sinto-me muito desconfortável a dar aulas remotamente. Não espero que nenhum aluno tenha a webcam e microfone ligado. Isso corta a comunicação não verbal por completo e isso faz toda a diferença no ensino. Quando dou uma aula presencialmente, eu vejo a cara de confusão deles quando vou a um ritmo muito rápido, ou o aborrecimento se estou num tópico demasiado tempo. Ou noto se estão distraídos no computador a ver outra coisa qualquer. Remotamente perco toda essa noção e sinto que estou a ir muito mais rápido (uma aula de 50 minutos é dada em ~30 minutos).

Uma segunda questão é a interactividade. A grande diferença no tempo é que eu faço questão de ir fazendo perguntas aos alunos durante a aula quase toda. Podem ser perguntas simples sobre o que acabei de dizer, perguntas mais complexas que exigem raciocínio sobre o que mostrei, ou perguntas sobre o que ainda não falámos, para levantar a curiosidade. Em aulas gravadas não há isto e é muito complicado fazer questões que façam o ouvinte pensar. O estado de espírito de quem vê uma aula no youtube não é a mesma. Em aulas em directo, os alunos vão levantando questões (tendem a preferir chat escrito. Eu próprio o preferia tendo em conta a latência e falta de qualidade em transmissões com muitos alunos) mas chegam-me normalmente fora do tempo ideal para as responder. Não por culpa dos alunos, mas porque eu falo rápido e demora tempo fazer uma pergunta por escrito. E a sensação de receber uma dúvida por email ou equivalente no final da aula sobre um aspecto fundamental do início da aula, faz-nos sentir horríveis em que o aluno deve ter perdido o resto da aula por lhe ter faltado aquela base. A probabilidade disso acontecer ao vivo é muito menor.

Se eu tivesse tido um ano para preparar esta cadeira em formato online (MOOC), teria melhorado estes aspectos? De todo. Aulas online são feitas para alunos que não têm dúvidas, ou que as vão tirar mais tarde de forma assíncrona. Exigem alunos super-motivados, algo que falta em geral nos nossos alunos do ensino superior e que é mais predominante em trabalhadores que pretendem adquirir uma skill específica. Esse parece-me o público-alvo dos MOOC.

Concluindo: a eficácia da transmissão de conhecimento ao vivo é muito maior. E não está relacionado com a complexidade do assunto, mas sim com a eficácia da comunicação não verbal e com o compromisso social de que se estão na mesma sala que o professor, estão a prestar-lhe atenção¹.

Falemos agora da avaliação. Eu uso projectos fora das aulas, alguns testes ao longo do semestre e exames que podem substituir estes testes. Os projectos podem continuar a fazer remotamente, embora o espírito de trabalho de grupo não seja o mesmo. Se profissionais com vários anos de experiência têm dificuldade a comunicar à distância [2], quanto mais alunos que estão a aprender o que estão a fazer enquanto o fazem… E o não ter de ficar mais umas horas na faculdade a fazer o trabalho e ter a liberdade de teoricamente poder fazer o trabalho em qualquer momento só faz com que ele desça de prioridade e fique para a véspera, quando será já tarde de mais para fazer o trabalho com o nível esperado de qualidade.

Quanto aos exames, foram propostas soluções baseadas em software proprietário que bloqueia o computador do aluno, forçando-o a apenas ver o teste, e um complemento que regista a webcam, microfone e ecrã e usa algoritmos de machine-learning para identificar possíveis padrões de plágio, que são posteriormente revistos por professores. Deixei de parte esta solução por dois problemas óbvios: nem todos os alunos têm webcam (e podem todos dizer que não têm), o que invalida a proteção contra estarem no telemóvel a trocar mensagens uns com os outros, e as questões de privacidade levantadas: será que essas gravações vão fora dos servidores da universidade? Não tendo uma resposta clara para esta pergunta, fica de fora esta alternativa.

Não há como garantir que a pessoa que faz o teste/exame é aquela que diz que entregou. Obriga-nos a confiar nos alunos, coisa que não fazemos (e por motivos históricos, com razão). O contexto de vários MOOC: profissionais que querem aprender uma skill em particular faz com que a avaliação não seja a parte importante (muitos até nem pagam o extra para terem a certificação, querem apenas concluir a parte lectiva e completar com sucesso o projecto) e com que a questão de ter sido aquela pessoa a fazer a avaliação ou outra não tenha importância.

Não imagino uma ordem dos médicos, engenheiros ou arquitectos a aceitar o curso online de alguém sem garantias foi esse alguém a prestar provas de avaliação.

Portanto o ensino presencial está para ficar, sendo que vão existir cada vez mais MOOC para conteúdos avançados, de reconversão e mais específicos.

¹Não tenho aulas de presença obrigatória nas minhas aulas, pelo que quem não estiver interessado é mais do que convidado a mudar-se para o bar mais próximo, onde poderá estar mais à vontade.

²As histórias que tenho com pessoas que não conseguem mesmo comunicar sem ser presencialmente…

I have been using filebot to automate the filing of TV shows and movies that are downloaded by my NAS into another folder structured by year, in the case of movies, and show and season, in the case of TV shows.

Unfortunately, the script stopped working because of some XML validation error.

Fetch failed: http://thetvdb.com/api/694FAD89942D3827/mirrors.xml
net.filebot.InvalidResponseException: Invalid XML: SAXParseException: The element type "hr" must be terminated by the matching end-tag "</hr>".
<html>
<head><title>301 Moved Permanently</title></head>
<body bgcolor="white">
<center><h1>301 Moved Permanently</h1></center>
<hr><center>CloudFront</center>
</body>
</html>

You can read more information about the issue at the forum.

The issue was that tvdb moved to https, and the script was trying to parse the page containing the redirect information. My first try was to replace all the static “http://” strings in the java byte code with “https://”. The real head-scratcher was that the mirror api was returning the “http” version of the api. If they moved towards https-only, all the endpoints returned by the API should also have changed. Anyway, more byte code to the rescue.

It is now working and you can download it here.

Foram publicados os resultados do CEEC 2018, onde apenas 8% dos candidatos conseguiram um contrato de 6 anos.

O Movimento 8% quer denunciar a precariedade na Ciência nacional e bem, até porque infelizmente ela é bem real. A existência de bolsas desrespeita os direitos de quem vive à custa delas (como eu já vivi) e considero até ilegal.

Mas o Movimento 8% está a usar or argumentos errados. Estão a basear a sua campanha em fotografias onde os sortudos que viram os seus contratos de 6 anos aceite estão a branco e o que não tiveram essa sorte a preto. Usar estas fotografias como meio de denúncia é enganador e inútil.

Em primeiro lugar, não ter ganho um contrato nesta call não quer dizer que não tenham um contrato de outra natureza para fazer Ciência. Posso dizer que no meu centro de investigação, todos os candidatos que não foram selecionados têm ou um contrato de post-doc associado a projectos de investigação, ou estão já integrados na carreira docente, onde não necessitam de se preocupar no que fazer quando acabarem os 6 anos.

É nisto que o Movimento 8% (com outro nome) se deveria focar: exceptuando poucos casos (humanidades e eventualmente matemática) é impossível fazer investigação sem ter financiamento para equipamentos, alunos, colaboradores, viagens a conferências, etc… Os investigadores FCT 2013 tinham até 50K€ para estes fins. Esses contratos não só pagavam o investigador, como financiavam alguns custos adicionais de forma a que fosse possível cumprir o plano de trabalhos.

E o movimento devia também focar-se em que não faz sentido dar contratos de 6 anos a pessoas que nas categorias de Investigador Principal e Coordenador estão no topo da sua carreira. Como exemplo, Maria Manuel Mota e Irene Pimentel foram deixadas de parte o ano passado. Nem as duas recipientes do prémio Pessoa, nem as respectivas instituições deveriam ficar satisfeitas com contratos de 6 anos. Investigadores Séniores não deviam sequer ter de se candidatar a estes concursos. Deviam ter um contrato com a instituição de acolhimento, com financiamento estrutural garantido pelo estado, tal como na carreira de docente o estado garante o financiamento dos professores.

E o que acontece quando o projecto que financia outros custos acabar, e o investigador só tiver o seu ordenado como garantido? Deixa de poder fazer investigação, mas tem emprego? Não faz sentido. Em vez do governo se preocupar em dar emprego a doutorados, devia-se focar em dinamizar a Ciência e dar condições para se realizarem projectos. E uma dessas condições é ter uma carreira em pé de igualdade com a carreira docente.

Agora gastar esforço a mostrar que um concurso que promove a precariedade teve uma taxa de aceitação de 8% é enganador para o público que não está por dentro disto, e mostra que os investigadores queriam esses contratos precários em vez de uma carreira a sério.

Foram recentemente publicadas alterações ao Estatuto do Bolseiro de Investigação, que rege a aplicação destas bolsas, usadas e abusadas por Universidades, Escolas, Fundações e Associações de cariz científico. Estas alterações foram publicadas para surpresa de todos os envolvidos no sistema de ciência nacional, e vieram muito àquem do que tinha sido prometido pelo ministro.

No entanto, estas alterações não vieram resolver a questão que sempre me preocupou: a aplicabilidade destas bolsas por Universidades e Centros de Investigação.

O estatuto abre com a definição do âmbito de aplicação das bolsas, e no primeiro artigo, ponto 5, pode-se ler:

É proibido o recurso a bolseiros de investigação para satisfação de necessidades permanentes dos
serviços.

Ora comecemos por analisar a tipologia que menos fazia sentido (e felizmente agora foi excluída), os Bolseiros de Gestão de Ciência e Tecnologia. Qualquer Universidade ou Centro de Investigação com mais de 20 investigadores necessita de alguém que faça a gestão e divulgação de ciência de forma contínua.

Quanto a bolseiros de investigação, não podiam (nem podem) ser usadas bolsas para financiar a investigação se for necessidade permanente de uma Universidade ou Centro de Investigação. A missão de qualquer centro de investigação é investigar, pelo que se excluí todas as bolsas de investigação, independentemente do grau.

Quanto às Universidades, as suas missões dividem-se em três pilares: Ensino, Investigação e Transferência de conhecimento e tecnologia. Quer as bolsas se enquadrem na investigação ou na transferência de tecnologia, cada uma dessas actividades representa cerca de 1/3 da missão, pelo que é uma necessidade contínua.

O caso menos óbvio são as bolsas de doutoramento (as únicas associadas directamente a um grau académico). Sendo que os doutoramentos concluídos é uma métrica de avaliação dos docentes, e estes se dedicam a 100% à investigação depois do primeiro ano, a tarefa que fazem é investigar e devem ser considerados como investigadores e portanto, produtores de algo necessário à missão da universidade.

O único caso seria outras instituições com outros fins (ex: repartição de finanças) oferecessem bolsas de doutoramento. Nesse caso deixamos de questionar a legalidade, mas sim a lógica de um estatuto só permitir isto.

Como resumo, bolsas de investigação nunca fizeram sentido nenhum. A nova alteração restringe o seu uso, mas ainda o permite de forma ainda mais inconsistente e apenas persistem porque permitem a um investigador realizar um projecto com mais recursos do que se tivesse de fazer um contracto. Mas isto são questões para um próximo artigo.

Which is to say, run some tests. You might just find that you’re getting enough performance out of your database that you can random-spray across your shards, have a stateless front-end and auto-scaled back-end and sleep sound at night because your nice simple system pretty well takes care of itself.

— Tim Bray – On Sharding

Tim (of Tim’s dumb affinity code fame) presented a shortcoming conclusion. Besides running some tests to evaluate several sharding alternatives, you also have to be employing talented engineers in your company, so they can adapt the system according to the dynamic needs of sharding.

And 50% of the traffic being generated by the top 10 clients is not much, when compared with the Pareto principle that these situations usually fall into.

Acho nojento olhar para a nossa bonita calçada portuguesa e ver beatas espalhadas por todo o lado. Esse cenário é infelizmente comum à volta de cafés, restaurantes e outros sítios de lazer.

É com bons olhos que vejo o projecto de lei apresentado pelo PAN e aprovado pela assembleia que proíbe atirar pontas de cigarro para a via pública e que, na sua redacção final, prevê coimas entre 25 a 250 euros. Apoio mesmo sabendo que na prática pouco vai mudar.

Mas o que me deixa mais chocado é que todos os edifícios onde é proibido fumar deverão dispor de cinzeiros e de equipamentos próprios para deposição dos resíduos indiferenciados e selectivos, sob pena de enfrentarem multas de 250 a 1500 euros. Não que tenha uma posição tão radical como a japonesa (no Japão, a reciclagem teve imenso sucesso à custa de que cada cidadão é responsável pelo seu lixo, tendo mesmo que o levar no bolso), mas acho ridículo que esta seja a prioridade dos nossos deputados.

Isto porque a lei do tabaco já foi actualizada várias vezes, mas nunca se aplicou a proibição de fumar a 5 metros da porta de locais públicos. Já houve tentativas, mas eram focadas em hospitais e escolas e sem nunca considerarem a aplicação de coimas.

Não me incomoda que existiram caixotes do lixo à porta de locais públicos (sobretudo locais de trabalho). Mas existirem cinzeiros é um convite a fumarem à porta de todos os edifícios (acentuado em dias de chuva), onde qualquer pessoas é obrigada a ser fumador passivo para sair ou entrar do seu local de trabalho.

Ao fim de contas, uma pessoa é obrigada a fumar para trabalhar, ainda que em segunda-mão, com todos os efeitos prejudiciais para a saúde que implica.

Acho bem que se multe quem atira beatas para o chão. Tal como acho prioritário que se multe os fumadores à porta de edifícios (ou esplanadas, ou paragens de autocarro, ou locais de reunião) antes de multar qualquer edifício público por não ter um cinzeiro.

A Visual Intro to NumPy and Data Representation

A nova lei europeia da directiva de direitos de autor foi aprovada pela comissão de assuntos legais. No final de março vai à votação a plenário.

Esta proposta foi feita por burocratas que não percebem nada da internet nem da forma como funciona. Não sei que peritos foram consultados, mas qualquer pessoa que perceba do assunto diria que isto é uma estupidez de todo o tamanho. Ou se calhar até disseram.

Escolham um dos deputados europeus que representam Portugal e liguem ou enviem email a pedir para votarem contra. Eles estão lá para nos representar! Eu já enviei o meu.

I remember the dark old times where IE6 was the default browser everywhere. Because of that dominance, developers focused solely on the IE substandard of JS/ActiveX/JavaApplet, leaving Linux and Mac users behind. Not long ago, you were required IE to submit your taxes. That has changed: Now you are required Chrome or Edge. As a Safari user, I find myself having to have an installed Chrome to access unsupported websites.

This week, MS announced they would be dropping their own rendered (EdgeHTML, a fork of Trident) on their current browser Edge and they will be using Chrome’s Blink (itself a fork of Webkit). So now the major browsers are:

• Edge (Webkit/Blink)
• Chrome (Webkit/Blink)
• Firefox (Quantum Render, replacing Gecko)
• Safari (Webkit)

Except for the tiny differences between vanilla Webkit and Blink, almost all the web uses the same renderer. This is the same monopoly Trident (IE5/6) had more than 10 years ago! And the sole fighter for a diverse web is the same browser and team that fought then: Mozilla Firefox! And this is not by chance: Mozilla’s Foundation is all about diversity and open standards. Just check their funded research projects to see that they put their money where their mouth is.

If it weren’t for Firefox, I believe Chrome would never had the success it had. Now Chrome’s the one that’s monopolising the web, and we need Firefox to be an alternative that will allow the NextBrowser™ to replace Chrome in 10 years.

I’ve been using Firefox as my main browser for a while now, and I can heartily recommend it. You should try it (and maybe talk to your relatives about it at Christmas). At this point, which browser you use no longer feels like it’s just about personal choice—it feels part of something bigger; it’s about the shape of the web we want.

— Jeremy Keith

If you’ve spent any time with graphic designers, you’ll know that they love spending your money on imperceptible tweaks to your image files. “It must be pixel-perfect!” they cry. When you query why they’ve generated the same icon in multiple sizes, each with subtle variations, they cryptically mention how everything must align with “the grid.”
This is hokum.

— The Myth of the Pixel Perfect Grid by Terence Eden

I have a couple of design friends that will keep on doing things pixel-perfect because of their OCD.

Microsoft has bought Github. This solves two problems for MS and two problems for GitHub.

The most insignificant improvement for Microsoft is that now they have expertise in git to solve the Windows mega-repository nightmare. The more important change is that they now have a piece of the development ecosystem that they have lost since Microsoft Visual studio became a boring concept (The recent Xamarin acquisition was the prequel for this move, more on this later).

For Github, this move has given them financial stability, as well as a new CEO. Why is this important? Well, a couple of years ago there were a string of harassment complaints at Github, including the CEO’s wife. Tom has since resigned. The new Ex-Xamaring New-Microsofty Nat comes from an open source background and has had quite a good run with Xamarin and its integration with MS tooling.

The hot question right now, is about the impact of this move on the Open-Source community, especially after a surge of project migrations to gitlab. Developers are afraid of what MS will do with Github, and are migrating to a more Open-Source alternative. While Github contributes to the community (libgit2, Atom, etc…), Gitlab develops its platform in open source (only the enterprise edition is closed source). This allows people (like me and my University) to host our own Gitlab instance, keeping all our (and our student’s) source code in-house. In case Gitlab.com ever closes, this is a better safe, than relying on Github to survive for ever.

What I am more concerned is the impact of developers migrating to Gitlab on the community. These migrations can go either smoothly (keeping a mirror on GitHub.com) or abruptly by deleting the repository on Github. I believe most of the cases will be the first, but I will consider the second for the sake of preparing for worst case scenario. Here’s what is going to break:

• Github-hosted pages (within GitHub subdomains)
• Other repositories that have the migrated repository as a sub-repo.
• Homebrew formula’s that build from source. I assume other source-based package managers will also suffer from this (emerge, Portage and pkgsrc).
• Python’s Pipfiles that depend on Github’s repositories will break. I assume the same for other language-level package managers.

Breaking the Cool URLs don’t die rule has a large impact on the community nowadays. A similar problem arised when _why committed online suicide and deleted all his repositories. All the ruby gems that depended on his were now broken. In his case it was an option, but you might be forced to migrate out of Github (it might close down one day if it goes out of business, or MS decides to go in other direction).

So how can one protect themselves against being too dependent on Github/MS or GitLab or whatever new fancy service? Well, it requires some DNS work. You should always own a domain that you use in your own repositories. This requires special support by Github/lab, similarly to DNS support by GitHub-pages, or what Tumblr or Soup.io do. This way, you can always change git provider (assuming you have a compatible Issues API, which Gitlab does and you can migrate public keys and access). This way you can migrate safely to another provider, without breaking all the dependencies on your code. Of course, just like backups, this has to be planned ahead of time, before announcing your git repo.

Surprisingly, this is not a new problem. Back in 2009, when considering the dubious Twitter management moves, people were thinking about how to move their micro-blogging to a distributed platform, so they could have different providers. Standards were developed and in the meanwhile, most of Twitter users moved to Facebook, an even more proprietary platform.

In conclusion, just like in the past, I don’t expected anything to change. I can’t see Microsoft closing down Github or even screwing it up. I assume they will merge Atom and VSCode, which share a common Electron code-base, which is really good news for Github, because Atom was lagging behind VSCode lately. MS and Github were already collaborating on Git VS/Windows tooling, and I expect that to continue. Git hosting will stay the same for MS, probably with an EE edition on Azure. I can’t really see this going wrong over the next 7 years.

I cannot sort by columns on my Mac 2016. It simply crashes Excel.app. I always thought it was strange for such important feature to be crashing.

Today I found out that Apple is patching the APIs that older apps from Microsoft (and many other developer) use. Sounds a lot like what Microsoft did in the last to an extent that it because impossible to maintain and test years laters.

From the long and interesting post:

Microsoft Excel/PowerPoint/Word have a patch in _CFArraySortValues to change the sorting algorithm slightly. How do you break sorting?!

I wonder if it has something to do with that Sierra patch (I’m running High Sierra).

Editorial note: I will start blogging more about technical content. This one is about my latest research paper.

Have you heard about the No Free Lunch Theorem? Basically it occurs when different solutions for a class of programs are not better nor worse than other solutions on average.

A non-mathematical example: if you have a great pasta chef, a great sushi chef and a great chimichanga chef, it’s a case of the “No Free Lunch Theorem”, and not because they will be expensive, but because if you ask them to prepare meals from the three cuisines, the quality will be equal on average (each one with a great meal and two so-so ones).

So this occurs in search and optimization algorithms, in which algorithms can be fined tuned for a given problem, but that extra-performance will not be seen in other types of search and optimization problems. Maybe the latest research on Transfer learning will show that this is not the case.

Back to my paper, it should evidence of the application of the theorem in the case of granularity control mechanisms for parallel programs. But what are those granularity control mechanisms?

When you write a divide-and-conquer parallel program, you split a program in two independent halves that you computer in parallel. But if you have more than 2 cores on your CPU, you can subdivide each half again, and you can now use 4 cores. And so until you can’t subdivide. But if you subdivide to have 1000 tasks, but you only have 16 CPU cores, your program will actually be slower! Dividing tasks and schedulinging each micro-task takes time, and doing that 1000 times is stupid. So the solution is to create as many tasks as you have CPU cores¹, right?

If only it was so simple. If a program being split in half would result in two independent tasks that take the same time to conclude, than the answer might be yes [2]. But there are several unbalanced or asymmetrical task graphs like this one:

In these cases, you have to create a dynamic condition that stops creating parallel tasks, and begins solving the problem sequentially. Here is an example program, using the Fibonacci example³:

The major research question of my PhD was to find the ideal function for that cut-off criteria. I proposed two new approaches and I have even tried to use Evolutionary Computation to find it for me, but I could never get to a function that would outperform all others in all of the 24 benchmark programs I have used.

So the answer to my PhD main Research Question is that it is impossible because this is a case of the No Free Lunch Theorem! There is no optimal cut-off criteria!

I could have given up on this, publishing a paper that would show that there is no answer, in order to prevent future PhD students to waste their time researching this topic like I did. But I ended up. not giving up on the big-picture problem here: Automatically optimizing parallel programs.

If there is no single cut-off criteria that is better than the rest, and typically there is one that is the best for each kind of problem, I took on the quest to automatically choose that best criteria for each problem. Using data from either my benchmarks, and random synthetic benchmarks, I applied Machine Learning Techniques to learn and predict the best criteria for future programs.

It’s 2018 and Machine Learning has saved the day once more [4]

1. Or hyper-threads, or CUDA cores, or OpenCL compute-units, of simply different machines.

2. But you still have to consider lock and memory contention.

3. Yes, this is a dumb implementation of fibonacci. It could be better either by being sequential or by using memoization. However, this dumb version is very asymmetrical and it’s hard to predict when its useful to stop parallelizing: it makes a wonderful hello world for this kind of problem.

4. Back in 2012 I have already applied Machine Learning to a very similar problem: deciding if a data-parallel program would execute on the CPU or GPU

Today my exFAT partition on my 1TB external hard drive died. I split that hard drive half-way for Time Machine (MacOS Extended (Journaled)) and exFAT for sharing large files with Windows machines with no stupid limits.

Disk utility was not helpful as it just hang when trying to repair the partition. And running any command-line utility gave me a “Resource Busy” error.

The solution:

ps -ax | grep disk2

with disk2 being the hard drive in question. Besides the grep process itself, you should kill all processes. Afterwards run:

sudo fsck_exfat -d /dev/rdisk2s2

with disk2s2 being the second partition of disk2. If should print a list of all the files in the drive as it fixes the filesystem (-d stands for debug).

Problem solved.

What is a signature

Desta vez a convite do João Cotrim, fui ao Geek Freak fazer parte de um painel sobre o Star Wars Ep 8 – The Last Jedi

If you aren’t aware of pixels.camp, it’s a 3 days hackathon in Lisbon, Portugal. This time I’m living 3 metro stops away, so despite not taking days off, I’ll be participating.

One of the bigger changes from previous editions is that a new voting system will be used, based on EXP, a closed crypto-currency on top of the ethereum.

Basic rules:

• If you are at the event, you get badges, each amounting to 100 EXP (I’m ignoring the variance here).
• There are angels who own a lot of EXP’s (25.000).
• There is one lucky guy who may win 50.000 EXP by solving a scavenger hunt.
• Participants can create projects.
• Everyone can invest in projects. The invested money is controlled by the organization.
• At the end of the event (and presentations), all the money invested in all the projects is redistributed proportionally to the 10 “richest” projects. These are the main winners of the event.
• After this, the EXP collected by each project are distributed by the investors proportionally to their investment.

I believe this approach is flawed.

Problem 1: Money is worthless at the end.

Unless you are one of top 10 (out of ~100) project owners or one of the X top investors, you get nothing. There is no actual interest in saving your money, or betting in low-risk investments. You want to hit the jackpot by investing in the number one project, if you are looking for winning the investor prize (I’m assuming the angels are out of the race).

Additionally, if you are the scavenge hunt winner, you should be extra careful with how you spend your money, not to lose it (because that money without investing is useless).

So, you should invest in the best company. The question is when.

Problem 2: Project presentations are in the end of the event.

There are no “investment” rounds here with no incentive for investing early. The best approach is to invest in the end, where you already have an idea of which projects have a chance of winning. What happens if everyone invests in the end? Maybe that’s the most fair scenario, but it is no different than a regular voting system without decentralized coins.

Problem 3: If you are competitive, you should invest in your own ideas.

If you really want to win this, it makes sense for you to invest early in your own project. If everybody does this, then the prize is only decided by the angels. Except if you do the right strategy:

• Get a small team of developers who are interested in doing something useful. Alternatively, create vaporware. Doesn’t matter as long as the angels are interested.
• Get a large team of miners, participants who are not interested in building something, but rather want to collect badges and participate in activities.

This will be the best approach towards winning (unless you have the best project according to the angel’s opinions).

Problem 4: There are no rewards in this Kickstarter.

The project presentation is supposed to work like Kickstarter. The most successful projects on Kickstarter had excellent rewards for investors. Here, unless you are rich, you have no real rewards.

If I end up creating a service as a project, I will give pre-access to the service to whoever backs me. If I am doing a prototype of something that will not last, there is no real reward I can give out (except free hugs).

Problem 4: Work vs Play

You should focus either on working (to get one of the 10 prizes) or playing (and getting badges to be a great investor). I don’t believe a half-way approach is very useful towards winning prizes (Although it might be the best fun experience).

Idea 1: VC-like groups.

Let’s say I invite everyone I know to a VC company. We decide amongst ourselves in which project we want to vote. Only the most voted project gets all the money from the group members. This might seem unfair for members who didn’t vote for it, but in the end it gives that project a better chance of winning, thus making VC members richer.

Btw, contact me in case you want to join Alcides&Friends Ventures, LLC. The larger the VC group, the larges the changes of winning a prize.

Idea 2: Betting

If you have been to previous editions (called Codebits at the time), you might remember the launch of a closed instance of Meo Wallet. It was the same idea, although projects didn’t ran on this. Rui and I won the prize for most money transferred, and came close second for the most money totaled (if only I hadn’t been so generous).

Idea 3: Ponzi scheme.

This was something we also worked on. I’ve known Ponzi schemes to last for months, and we only need it to last 3 days. So contact me as soon as you can to be one of the first to take advantage of the Alcides scheme™.

Don’t get me wrong, this is an interesting idea and we should use these events to play with ideas like this. But I have my doubts it will work in the end like it is intended to.