I am always struck by the strange quirks of #Dafny imperative and functional syntax:

Take the syntax for function/method prototypes:

```
method Foo(a : int, b : int) returns (res : int)
function foo(a : int, b : int) : int
function fooAlt(a : int, b : int) : (res : int)
```

and now anonymous functions:

```
method Foo<A>(f : (A) -> B, a : A) returns (res : B)
```

I wish Dafny would have some sugar that harmonises the use of `->` above in favour of `:`. Colon implies 'has type' not returns a type...

```
Foo(a : int, b : int) -> (res : int)
```

Urgh #Dafny and #NixPkgs still not playing nicely...

Downloading direct from Github I get a working compiler.

Installation through NixPkgs means the resulting binary cannot find the local #dotnet install...

On my course, students like to say they know python.

I wonder how they feel about this:

https://gist.github.com/jfdm/fbb1f88065ab97b3c8e57ef322b1720e

*Four*

Urgh, our Office365 web interface has a shiny button for Copilot...

Can we just not...or at least have an option to hide it...

Whilst I do not like tooting my own horn, if you were interested in my #TYPES2025 talk (Towards Being Positively Negative about Dependent Types) and could not make it.

Here you go:

https://www.youtube.com/watch?v=8xc50Lf6pXs

I hear ICFP is going to get FREX'd but with the meeting of two conferences, fools seldom differ!

Well done all.