Jesper Agdakx 🔸

As part of our (@sarantja@mastodon.social and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.

We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.

Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS

You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).

P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.

#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey

The joys of booking European train tickets: travel from Delft to Rzeszow edition.

• Look up tickets on bahn.de: well 23h of uninterrupted trains seems excessive, how about we make a stop in Berlin?
• Actually I heard there’s a sleeper train to Berlin, let’s check it out!
• Oh the only place I can book it is in europeansleeper.eu, fine I guess.
• Sleeper train only goes on specific days of the week. Well there’s one on Friday, then we can stay one day+night in Berlin before continuing to Rzeszow, perfect!
• For the way back there’s a sleeper on Sunday night, that works as well.
• Great, I have tickets for the sleeper, now let’s get the tickets from Berlin to Rzeszow!
• Uh oh: “Unfortunately, a reservation is not possible for this connection. Due to compulsory reservation, a booking is therefore not possible. Please choose another connection.” WTF?
• Let me try the Polish railway instead. What’s the website? Oh here’s polishtrains.eu, that looks plausible.
• [after entering a whole bunch of information, just before payment] “Attention! The carrier’s tariff conditions have changed. Please check the details before purchasing.”
• Ok sure, I’ll check the changed conditions. Let me pay now.
• “Attention! The carrier’s tariff conditions have changed. Please check the details before purchasing.”
• WTF?
• “Attention! The carrier’s tariff conditions have changed. Please check the details before purchasing.”
• Searches the internet
• Ok so I need to book the tickets on intercity.pl instead of polishtrains.eu? Of course, silly me.
• Well this website is not very well translated, but I’ll manage.
• I cannot buy a return ticket but need to buy two separate tickets, how annoying.
• [after buying the outbound ticket] “No offers fulfil the criteria.”
• Uhm hello I can see you have a train scheduled for this day, I would like to buy a ticket please?
• “You are purchasing a ticket well in advance. The departure station and time, as well as the arrival station and time, may change.”
• Well I guess that means I’ll just have to try again next week, I guess?

So the current status is that I spent too much time on this and have 3/4ths of my trip booked.

#Train #Railway #PublicTransport #EuropeanSleeper #EuropeByRail