Alcides Fonseca

Early at the WITS workshop at this year’s POPL I presented why we need to improve the error messages of languages with liquid types, in order to increase adoption. This presentation resulted from our experiences using (LiquidHaskell) and developing (Aeon, LiquidJava and MLVP) languages with liquid types. They are very useful to have guarantees of correctness, but you usually don’t know if it is an error in the usage of functions, or in their specification. We end up proposing some suggestions to improve the state of the art, in which we are working on.

The video:

And the slides:

Getting a M1 Max MacBook Pro, I had to figure out how to install all the software I had on my old Intel Mac. One of the most challenging was LiquidHaskell. Here are the instructions for others to save some time.

Install z3

LiquidHaskell requires an SMT solver to handle constraint-solving. Z3 is my go to solver.

brew install z3
z3 --version
# Z3 version 4.8.14 - 64 bit

Install LLVM 12

Because of this bug in homebrew’s LLVM 13 that solves other problems, we need LLVM 12.

brew install llvm@12

Install latest version of stack.

The stable version of stack will not install GHC on OSX arm installations. To overcome that, we need to install the latest version.

brew install --HEAD stack

Setup a Demo Repository

I recommend using this scaffold project to get LiquidHaskell running on the command line and VS Code. It might work on other editors, but I have not tested them.

git clone https://github.com/alcides/lh-plugin-demo.git
cd lh-plugin-demo
stack build
stack ghci

This last line should open ghci, doing all the liquid type verifications necessary. You should see two green lines with 1 and 3 constraints checked, respectively.

You can do the exercise of editing src/Demo/Lib.sh and changing x + 1 to x - 1 and running the command again. You should now see an error.

VSCode Configuration

Now that we have error reporting on the command-line, we can move to the more convenient code editor. In my case that means VSCode¹.

The first step is to uninstall all Haskell plugins. Just trust me on this, they are all pretty much incompatible with each other, except when they aren’t. Now you need to install Simple GHC (Haskell) Integration. On the CLI:

brew install visual-studio-code
code --install-extension dramforever.vscode-ghc-simple

However, this will not work for a M1-unrelated reason: LiquidHaskell and Haddock are not compatible (unfortunately). So the first step is to disable it.

Go to Settings > Extensions > GHC Simple config > Ghc Simple > Startup Commands and remove :set -haddock.

Cmd+shit+P and select GHC: Restart GHCi Sessions if it doesn’t restart on its own.

And now you should have localized errors in your Haskell files.

¹Textmate’s support for Haskell is pretty minimal. Stack and Cabal support is completely missing.

Suppose, for example, that your driver’s license is on your mobile phone. (...) You no longer need to go to a government office to get your new driver’s license. However, it now makes it possible for a civil servant to decide that you cannot drive your car on Tuesdays. They do not need a new law, they do not need your consent, they can just switch a flag inside a server.

— Enforcement by Software by Daniel Lemire

This is something that has been worrying me, especially in the cases where software doesn’t follow the law and leads tens or thousands of users to follow processes illegally, just because there is no other way of doing it. Maybe society should invest more in legal verification of software and processes.

I upgraded to a new M1Max MacbookPro (will have to review it next), and I had to install lean4 today. Unfortunately, elan does not work in the M1 architecture as expected, so I had to use rosetta. here’s how I set it up:

1. Install VSCode: brew install --cask visual-studio-code && code --install-extension jroesch.lean
2. Install Rosetta2 /usr/sbin/softwareupdate --install-rosetta --agree-to-license
3. Install elan manually: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | arch -x86_64 sh
4. Install latest lean: elan default leanprover/lean4:nightly
5. Configure the lean path in the lean4 vs code extension to point to this lean: “Lean4: Executable Path” to arch -x86_64 lean

It will work. Now let’s hope that elan adds supports for arm64 binary fetching.

When I’m looking for potential students, I always try to identify T-shaped people: those who can go deep into one topic, but also have a broad view of other aspects of Software Engineering. But what Bastien Rieck says is completely true.

In any case, many graduate schools and resume reviewers tend to ignore the breadth of a person’s skills, focusing instead only on the depth.

T-Shaped People and Academia, by Bastien Rieck

T-shaped people not only help in several aspects of the development of a project, but also identify bridges with other areas, and allow your work to be applied to other problems.

Today I got the following error when executing regular numpy code in my homebrew Python3.9 installation.

ImportError: dlopen(/usr/local/lib/python3.9/site-packages/scipy/linalg/_fblas.cpython-39-darwin.so, 0x0002): Library not loaded: /usr/local/opt/gcc/lib/gcc/10/libgfortran.5.dylib Referenced from: /usr/local/lib/python3.9/site-packages/scipy/linalg/_fblas.cpython-39-darwin.so Reason: tried: '/usr/local/opt/gcc/lib/gcc/10/libgfortran.5.dylib' (no such file), '/usr/local/lib/libgfortran.5.dylib' (no such file), '/usr/lib/libgfortran.5.dylib' (no such file)

The issue was that I had gcc 11 installed (you can check via brew info gcc), but homebrew-installed bumpy expected gcc 10 to be installed.

Reinstalling numpy from bottle or from source didn’t work.

The workaround:

brew install gcc@10
sudo ln -s /usr/local/opt/gcc@10/lib/gcc/10/libgfortran.dylib /usr/local/lib/libgfortran.5.dylib  
sudo ln -s /usr/local/opt/gcc@10/lib/gcc/10/libquadmath.0.dylib /usr/local/lib/libquadmath.0.dylib

For the 4th year in a row, I am teaching Parallel and Concurrent Programming. One of the main sections of the course is general-purpose GPU programming (GPGPU), where I mostly use CUDA, but I also show them how to the same using OpenCL, bindings in Java and Python, as well as Numba. For their projects, all students use either CUDA or Numba.

Because we want to provide students with access to a GPU, even if outside campus, we show them how to use Google Colab, a Jupiter Notebook environment with optional GPU or TPU, and it has been working fine for 3 straight years.

When preparing this week’s class, I ran the examples on my local machine and it all worked. Fast forward to the lab, and I was demoing the usage of Google Colab and it wouldn’t work. In panic, I gave students temporary access to my machine while I debugged the issue.

The Example

I’m still using the code prepared by NVIDIA’s Nuno Subtil for the GPGPU workshop we organized back in 2011. It is a simplified version of the NVIDIA examples, with a very handy HANDLE_ERRORS macro that checks the return code of each cuda function (cudaMalloc, cudaMemcpy, cudaFree. The example in particular would take two arrays A (containing elements from 0 to 1000) and B (from 1000 to 0) and would return the array C, with the sum of the corresponding positions in both arrays.

The Error

The program would output an array of all zeroes. CUDA functions return 0, showing they are working correctly. I reviewed all the code and it should work. And it worked on my machine ( famous last words ).

Finding the Error

After modifying the arrays manually to check where the error was, I restricted it to the kernel call. And it made sense, it was the only call whose result wasn’t being checked. Knowing this, I’ve added line 47 to understand the error: Device Variable Copying: no kernel image is available for execution on the device

Understanding the Error

Kernel is the name of the main function that executes on the GPU and it is called from the CPU using a kernelName<NTHREADS>(args). The kernel image should be the binary on the GPU that will be execute. If it isn’t there, the kernel does nothing. But the program continues silently. This is a really bad design decision on their part.

Fixing the Error

Because different GPUs support different binary versions (due to architectural differences), I tried to compile to the right architecture. Google Colab gave me a Tesla K80, which worked with SM_37 and compute_37. I’ve added those as flags in the mvvm compiler:

!nvcc -arch=sm_37 -gencode=arch=compute_37,code=sm_37 vector-sum.cu -o vector-sum

And it now worked. Why is this required? Because Tesla K80 is only supported between CUDA 5 and 10. Google Colab is running on CUDA 11 (despite providing unsupported GPUs) and users get silent errors.

Spending 30 minutes juggling debugging this issue while giving students a fallback alternative was very stressful. I mostly blame Nvidia for not having a better exception handling of kernel calls. There’s also a little blame in not supporting old cars in new SDK versions (even if not supporting all features). Google also shares the blame by loading a version of CUDA incompatible with the provided GPU.

During my PhD, my advisor and I disagreed about the spelling of runtime/run time. There was no definite answer as different papers used different spelling in different usages. This week I found a rationale that makes sense to me, even if it means that we were both wrong.

There are three variants of the word “run time” in computer science:
run-time — adjective (“the run-time performance”)
run time — noun — a moment in time (“occurs at run time”), or an amount of time (“the run time is 8 hours”)
runtime — noun — a program that runs/supports another program (“the runtime handles memory allocation”); a synonym for “runtime system”

I am (re)writing an implementation for the Refinement Types tutorial by Ranjit Jhala and Niki Vazou. I am hoping that it helps others understand these concepts, and promote this research among your researchers.

I am streaming its development on Twitch, so if you are interested make sure you either have your notifications turned on, or you follow me on Twitter.

Chapters:

• 5-minute intro to Refinement Types
• Checking the Satisfiability of Liquid Terms with Z3 (Code)

Here are a few resources for plotting scientific data that is accessible and accurate.

• Creating publication-quality figures with Matplotlib — A great tutorial on different aspects of plotting, with matplotlib examples.

• Creating Reproducible, Publication-Quality Plots with Matplotlib and Seaborn — Another tutorial, focused on the reproducible aspects of plotting, with Matplotlib and Seaborn examples

• Visualization of Color Palettes using Maps Notice the sequential, divergent and qualitative options as those are crucial.

• YellowBrick — A matplotlib-based library for data-science. It has several templates for evaluating classifiers, exploring data, ...

• missingno — A visualization library for understanding missing data in datasets.

• LovelyPlots – A theme for beautiful and TeX-compatible matplotlib themes.

The current approach for having a complex Haskell project with dependencies is using stack. While it is suitable for larger projects, we avoid it for our undergrad students, who only need ghc, ghci and small editor support.

We found a subset of VSCode plugins that provide an integrated interpreter, provide type information, autocomplete and even runs (sometimes too strict) hlint on your code automatically. Neither of this plugins requires Stack.

The main issue is that we teach QuickCheck and we need to install it globally. This is far from being straightforward in Windows and MacOS.

In Ubuntu it is quite direct using apt sudo apt-get install hlint haskell-platform libghc-quickcheck2-dev

Here is the solution for the Mac, just make sure to adapt to your own GHC version:

brew cask install cabal-install
ln -s ~/.cabal/store/ghc-8.10.1/package.db ~/.ghc/x86_64-darwin-8.10.1/package.conf.d
cabal install QuickCheck

If you now open ghci, it will import Test.QuickCheck successfully.

For reference, here are the plugins that work successfully without any Stack dependencies:

code --install-extension jcanero.hoogle-vscode
code --install-extension justusadam.language-haskell
code --install-extension hoovercj.haskell-linter
code --install-extension dramforever.vscode-ghc-simple
code --install-extension meowcolm024.has-go

Over the last couple of years, I have spent a significant amount of time browsing and scoring resumés (Vitae is the common name in Portugal) for different positions, both in academia and industry. The majority of those had been poorly designed. In this post, I try to help you design the perfect resumé, and avoid common pitfalls. While this is designed towards Software Engineering, you might find this relevant for other areas.

The Header

You should have your basic information on the top of your CV: Name, email address, location and optionally phone number. A few tips:

• If your student email is something like sch34134123@..., please use a personal email address instead.
• Never use your current employer’s email. Use a personal email address.
• Do not use your full address. Your street number is useless for this purpose and you don’t want your personal information on the internet. Just list your current city/county.
• I would suggest having the Country specified, as it helps companies in understanding if they can’t hire you (due to visa and immigration issues).

Things you should omit from the header:

• Gender, marital status, number of children, religion and other information that could be used for discrimination.

Things you may or may not include in the header:

• A plain (meaning non-party) picture. I would suggest towards including if there is an expectation that the hirer would know you (e.g. if you are applying for a research grant with a professor).

First things first.

The next two sections are Education and Experience. If you do not have real-world experience or if you are applying to an academic position, you should have Education first. Otherwise, I would have Experience first.

Experience

Experience should come in reverse chronological order. Have your last (or current) job first. This is usually what most recruiters will focus on. Besides the start and end dates, title and company, you should have a small paragraph explaining what were the main activities and responsibilities of your position. If you were a software developer, you should explain what kind of software you worked on, and what was your contribution. Some people also like to include technologies they have worked on, which works well with HR people.

If you had odd-jobs outside your field, please leave them off the first page and in “Other Experience”. Not that you should feel ashamed of them, but let recruiters focus on what’s important for the role they are pursuing.

Education

Stick with reverse chronological order. If you are currently taking (or just signed up for) a degree, please include it, as well as the expected graduation year. If you have other degrees like Biology or Music Theory, please leave them off the front-page (and move them to Other Education) except if that might be relevant for the job application! Examples would be a company that works on software for DNA processing, or on software for Audio Synthesis.

For each degree, you should list your average grade, as well as highlight the top 5 or top 10 courses in which you had the best grades, or which are relevant for the job application.

Projects

This section is specific for Computer Science and it is only relevant if you do not have a lot of experience. In this case, you should write one paragraph about the projects (even if it’s coursework) that you did, what technologies you used and what you learned. 3 projects are more than enough, and if they were developed outside course work (opensource or in a research environment), it’s more valuable. Include a link for the code repository (Github or similar), making sure you already have the final grade for that course.

Other Activities and Awards.

You can have some other activities listed in your CV, but make sure they are relevant for the job if they are in the first page. As a rule-of-thumb, you should list those that reveal organizational or leadership. Being a casual chess player is not a relevant activity (It’s actually a hobby, and you should leave it off the Resumé) but being the President of your local Chess chapter can be relevant.

Final Remarks

Show your CV to more senior colleagues and even professors and ask for feedback. You want your CV to shine compared to those Europass form-generated CVs.

As an example, you can look at my CV in 2011 (I also had a cooler web version).

More resources:

• OpenAcademics resources for CVs, Personal Statements and more

Muito se tem escrito sobre os catedráticos da NovaSBE não quererem que se assine artigos de opinião com o nome da escola.

Ora eu cá acho que falta trazer o argumento mais importante à discussão: para se ler um artigo de opinião é necessário perceber o background do autor. Vou ler um artigo de forma diferente se souber que é uma parte interessada do tópico. Não só o autor deve identificar o(s) cargo(s) que exerce e onde, como também mencionar a relação directa com os intervenientes da peça que está a escrever (ex: a empresa XPTO é mecenas da universidade a que pertenço, embora não tenha relação directa).

Como exemplos de autores que levam esta transparência a sério, têm James Governor e Tim Bray. Os seus artigos identificam claramente onde existem conflitos de interesse, muitas vezes especificando a relação (“empresa x é cliente, mas não trabalhamos com esta divisão da empresa” ou “trabalhámos em tempos com a empresa X, mas não temos qualquer relação actualmente”).

Claro que o bottom line desta discussão é se as universidades públicas deveriam estar assim tão dependentes financeiramente de privados (que é a origem deste assunto ser sequer debatido). Claro que não, mas para resolver isso é necessário que o governo aumente o orçamento destas instituições.

Sobre este assunto, há uma carta assinada por 50 cientistas e 50 empresários (e a crescer) a pedir que se faça um investimento contínuo e de base para a ciência em Portugal.

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.