As much as #Dafny intrigues me, the Dev UX is strangely buggy for me. (Trying to hook in an externally written library and every thing is falling apart)
What is worse, the version in Nix appears to be packaged wrongly, (won't recognise dotnet) and I have to resort to binaries from GitHub!
Who da thought! Having multiple distinct uses of `(=)` in your language would be confusing...
For assignment, as a type, and for equations...
Might start not using `(=)` as the type for equality, and use `(===)` more...
Perhaps, for next generation of #Idris , it would be good to have a proper user study on what is appropriate syntax for key aspects of the language.
The strangeness budget for imperative programmers in #CS886 has been blown! The students are warming to #Dafny more! (Rapid introductions aside) The reaction towards the two languages was expected. They do not have a functional, nor PLT background.
I should talk to colleagues about their experience in the other course....
The more I use #Dafny (for teaching) the more I realise that it is, perhaps, too smart and too complex for its own good.
I spent 20+ mins working out how to make a class field private.
20mins reading documentation & a few more minutes fighting syntax.
Whilst, at times, I ain’t the sharpest tool in the box, this does take the cake…
For instance (note I was talking about #Dafny and exploring Design-by-Contract)
The first smart chapter summary:
```
# Exploring Daphne and Emacs Usage
Jan expressed frustration with computers and shared his preference for using Emacs over VS Code. He demonstrated how to use Daphne, a multi-paradigm language, emphasizing its object-oriented and imperative programming capabilities. Jan highlighted that Daphne's main method is where program logic resides and that functions can be side-effect-free. He also mentioned his intention to write a program that computes the absolute value of a number.
```
I have managed to get hings working by rolling back to earlier versions.
The bump in #Dafny between 4.7.0 and 4.8.0 hasn't helped either.
Neither is being able to get a single executable generated when running `dafny build`.
#Dafny sadly doesn't have support for #literate_programming a cool feature I think they should support!
Whilst I do not think libraries nor programs should be coded in the literate style, informal presentations and lectures and notes should be!
For #Idris, I have often wrote the presentation in OrgMode and used polymode to mix orgmode and idris-mode together.
Org-mode provides more precision on revealing items and storing reading notes. (one step away from writing that book as well...)
Idris' own mode enables interactive editing.
Key for polymode to work is that the compiler must be literate enabled.
I found a solution through someone's notes on a code sharing platform. Sadly, these notes are not licensed :-(
Not having Reading from STDIN when you can Print to STDIN is not great. #Dafny is not pacman complete.
You need that for shits & giggles, a semi-decent Std Lib too...
#Dafny users, if I wanted to write an interactive program that has a REPL: What support _is_ there for reading from STDIN? The STD library only has file io...
Cursed #dafny I think I need to stop...
```{.dafny}
function fromString(s : string) : Maybe<CMD>
{
bindM(cons(s), (x : (char,string)) =>
if x.0 == ':'
then bindM(cons(words(x.1)), (y : (string, seq<string>)) =>
decide(y.0,y.1))
else Nothing)
}
```
All I wanted was a pure computation context...
Playing with #Dafny (the language) and it’s interesting how there is a mix between pure functional code and imperative code. I cannot, quite, get the idioms or intentions between when I should use imperative over functional. The Functional programmer,l always goes functional…
Reason \((S n)\) as to why I am not fond of #programming #font #ligatures:
+ \(\in\)
+ \(\notin\)
Look the same for me at my usual font size...
#Dafny mode for emacs uses a 'pretty mode' by default (Boo!), worse is that the option is not customisable (BOO!).
```{.elisp}
(defun no-prettification-in-dafny-mode ()
(prettify-symbols-mode -1))
(add-hook 'dafny-mode-hook #'no-prettification-in-dafny-mode)
```
Interesting afternoon playing with #Dafny core concepts. [1]
I am teaching Dafny next semester.
I do not think I will be teaching much much more than the core concepts. (FP, imperative programming, basic proofs, State, Frames, Basic Ghosting), Nothing fancy with ghosts nor proofs nor OO.
Just too much to do in a course with the audience I *think* I have. (Some people like to push students hard; I do not)
I also think I wll go against my gut and lecture half with slides (overview and paradigms) and half live coding (explore the fundamentals).
Revisiting thinking of using #stacscheck [1] for #goldenfile testing of projects.
The language of assessment (#dafny) doesn't seem to do goldenfile testing 'out-of-the-box', and internal unit-testing is not what I 'want'.
Sadly, I wasn't aware of the `lit` program [2] which _was_ used by dafny, and so not available on lab machines.
Tempting to revisit and extend a haskell based setup derived from Idris(1) test suite I used when at Glasgow, or co-opt idris2's test suite for it all...
Teaching is fun...
[1] https://github.com/ChrisJefferson/stacscheck
[2] https://llvm.org/docs/CommandGuide/lit.html
#Dafny users, is there a standard way to perform 'whole program' golden file testing of dafny executables?
That is, I want a suite of tests to pass input to a program and compare output with expected output. As we do in Idris2 https://github.com/idris-lang/Idris2/tree/main/tests
dafny-annotator: AI-assisted verification of Dafny programs. ~ Gabriel Poesia, Chloe Loughridge, Nada Amin. https://arxiv.org/abs/2411.15143 #LLMs #Dafny #FormalVerification
