#Teaching both #Dafny and #Idris, not to a deep level mind, to those at intermediate level of programming.

I am taking lots of copious anecdotal notes of students and their struggles, as I think we can do better with Idris (and Dafny) to make the languages more accessible. Need some more qualitative work to ensure that we do the right thing though...

Dafny: Verification-Aware Programming Language

https://dafny.org/

#HackerNews #Dafny #Verification-Aware #Programming #Language #Programming #Languages #Code #Verification #Software #Development

For those that like #Dafny, I am working on porting the documentation to a sphinx project. Fortunately, sphinx supports markdown through myST.

Hopefully when I am finished (including PDF generation of the reference doc) we can look at getting it into Dafny itself...

Of course the code crashed, 'twas better crashing than other forms of runtime corruption....

That aside, it would be better if the error was picked up at compile time.

Par example, some #Dafny code, where the last `print` statement fails because we cannot guarantee at compile time that x is okay...

```
datatype Result<E,T> = Error(msg : E) | Ok(value : T)

function unwrap<E,T>(res : Result<E,T>) : T
requires res.Ok?
{
res.value
}

function safeDivide(a : nat, b : nat) : Result<string, nat>
{
if b == 0
then Error("You've encountered a Wild Zero.")
else Ok(a/b)
}

method Main()
{
var x := safeDivide(1,0);
var y := safeDivide(4,2);

print unwrap(y), "\n";
print unwrap(x), "\n";
}
```

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...